Theorem syl6ibr 151

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 124	. 2 ⊢ (χ → θ)
4	1, 3	syl6 29	1 ⊢ (φ → (ψ → θ))

Syntax hints:   → wi 4   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  3imtr4g  194  imp4a  331  dcbi  832  oplem1  870  3impexpbicom  1306  hband  1359  hb3and  1360  nfand  1442  nfimd  1459  equsexd  1599  euim  1950  mopick2  1965  2moswapdc  1972  necon3bd  2226  necon3d  2227  necon2ad  2240  necon1abiddc  2245  ralrimd  2375  rspcimedv  2635  2reuswapdc  2720  eqsbc3r  2796  ra5  2823  difin  3151  r19.2m  3286  tpid3g  3457  sssnm  3499  ssiun  3673  ssiun2  3674  sotricim  4034  sotritrieq  4036  tron  4068  ordsucss  4180  ordunisuc2r  4189  ordpwsucss  4227  dmcosseq  4530  relssres  4575  trin2  4643  ssrnres  4690  fnun  4931  f1oun  5071  ssimaex  5159  chfnrn  5203  dffo4  5240  dffo5  5241  isoselem  5384  fnoprabg  5525  poxp  5775  issmo2  5826  smores  5829  tfrlemibxssdm  5862  swoer  6045  qsss  6076  recexprlemm  6458  recexprlemloc  6465  recexprlem1ssl  6467  recexprlem1ssu  6468  recexprlemss1l  6469  recexprlemss1u  6470  bj-omssind  7157  bj-om  7159  bj-inf2vnlem3  7190  bj-inf2vnlem4  7191