Theorem syl6ibr 218

Description: A mixed syllogism inference from a nested implication and a biconditional. Useful for substituting an embedded consequent with a definition. (Contributed by NM, 5-Aug-1993.)

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	biimpri 197	. 2 |- (ch -> th)
4	1, 3	syl6 29	1 |- (ph -> (ps -> th))

Syntax hints:   -> wi 4   <-> wb 176

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

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  3imtr4g  261  imp4a  572  3impexpbicom  1367  nic-ax  1438  nfimd  1808  equs5e  1888  euim  2254  mopick2  2271  2moswap  2279  2eu1  2284  necon3ad  2553  necon3d  2555  necon1d  2586  ralrimd  2703  spcimegf  2934  spcegf  2936  spcimedv  2939  spc2gv  2943  spc3gv  2945  rspcimedv  2958  eqsbc2  3104  ra5  3131  tpid3g  3832  pwpw0  3856  sssn  3865  pwsnALT  3883  ssiun  4009  ssiun2  4010  spfininduct  4541  dmcosseq  4974  ssreseq  4998  ssrnres  5060  fnun  5190  f1oun  5305  fvopab3ig  5388  chfnrn  5400  dffo5  5425  fvclss  5463  fnoprabg  5586  ovigg  5597  leltctr  6213  spacind  6288  fnfrec  6321