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	⊢ (φ → (ψ → χ))
syl6ibr.2	⊢ (θ ↔ χ)

Assertion

Ref	Expression
syl6ibr	⊢ (φ → (ψ → θ))

Proof of Theorem syl6ibr

Step	Hyp	Ref	Expression
1		syl6ibr.1	. 2 ⊢ (φ → (ψ → χ))
2		syl6ibr.2	. . 3 ⊢ (θ ↔ χ)
3	2	biimpri 197	. 2 ⊢ (χ → θ)
4	1, 3	syl6 29	1 ⊢ (φ → (ψ → θ))

Syntax hints:   → wi 4   ↔ wb 176

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 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  2552  necon3d  2554  necon1d  2585  ralrimd  2702  spcimegf  2933  spcegf  2935  spcimedv  2938  spc2gv  2942  spc3gv  2944  rspcimedv  2957  eqsbc3r  3103  ra5  3130  tpid3g  3831  pwpw0  3855  sssn  3864  pwsnALT  3882  ssiun  4008  ssiun2  4009  spfininduct  4540  dmcosseq  4973  ssreseq  4997  ssrnres  5059  fnun  5189  f1oun  5304  fvopab3ig  5387  chfnrn  5399  dffo5  5424  fvclss  5462  fnoprabg  5585  ovigg  5596  leltctr  6212  spacind  6287  fnfrec  6320