Theorem syl6ibr 186

Description: A mixed syllogism inference from a nested implication and a biconditional. Useful for substituting an embedded consequent with a definition.

Hypotheses

Ref	Expression
syl6ibr.1	|- (ph -> (ps -> ch))
syl6ibr.2	|- (th <-> ch)

Assertion

Ref	Expression
syl6ibr	|- (ph -> (ps -> th))

Proof of Theorem syl6ibr

Step	Hyp	Ref	Expression
1		syl6ibr.1	. 2 |- (ph -> (ps -> ch))
2		syl6ibr.2	. . 3 |- (th <-> ch)
3	2	biimpr 134	. 2 |- (ch -> th)
4	1, 3	syl6 23	1 |- (ph -> (ps -> th))

Syntax hints:   -> wi 2   <-> wb 127

This theorem is referenced by:  imp4a 282  elimant 505  19.23 745  hband 788  mopick2 1057  2moswap 1064  2eu1 1067  r19.21ad 1261  cla4egf 1395  cla42gv 1399  rax5 1472  sssn 1852  pwpw0 1883  ssuni 1937  dfwe2 2187  wefrc 2195  ordsseleq 2227  ordtri3or 2230  ordtri3 2234  ordon 2238  tfis 2245  ssorduni 2249  oneqmini 2272  onmindif2 2313  nnsuc 2389  tfinds 2401  relss 2480  opeldm 2534  relssres 2596  cotr 2625  cnvsym 2626  funss 2682  fnun 2730  f1oun 2815  fvopab3ig 2869  chfnrn 2885  fvclss 2907  isomin 2937  isofrlem 2939  f1oweOLD 2944  rdglim2 2987  tz7.48lem 2993  tz7.49 2997  oprabvalig 3048  infsdomnn 3426  pssnn 3428  inf3lem4 3467  rankr1 3518  r1pwcl 3530  aceq5lem4 3561  aceq5 3563  aceq6b 3565  ac5b 3574  kmlem2 3581  zornlem4 3606  zornlem6 3608  zornlem7 3609  fodomb 3615  imadomg 3616  cardne 3637  carden 3638  carddom 3642  alephordi 3679  cardaleph 3690  carduniima 3695  cardinfima 3696  cflim 3704  indpi 3828  ltaddpq 3873  genpcl 3905  prlem934 3933  ltaddpr 3934  ltexprlem1 3936  ltexprlem5 3940  reclem4pr 3953  suplem1pr 3955  axrecex 4079  axsup 4088  zaddclt 4590  zmulclt 4596  zneo 4601  uzwo 4605  nnwoOLD 4608  nn0opth 4724  sqr2irr 4782  shmods 5363  orthin 5371  spansneleq 5475  h1datom 5483  osumlem4 5533  stcltr2 5708  sumdmdi 5785

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128

metamath.org