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  843  oplem1  881  3impexpbicom  1324  hband  1375  hb3and  1376  nfand  1457  nfimd  1474  equsexd  1614  euim  1965  mopick2  1980  2moswapdc  1987  necon3bd  2242  necon3d  2243  necon2ad  2256  necon1abiddc  2261  ralrimd  2391  rspcimedv  2652  2reuswapdc  2737  eqsbc3r  2813  ra5  2840  difin  3168  r19.2m  3303  tpid3g  3474  sssnm  3516  ssiun  3690  ssiun2  3691  sotricim  4051  sotritrieq  4053  tron  4085  ordsucss  4196  ordunisuc2r  4205  ordpwsucss  4243  dmcosseq  4546  relssres  4591  trin2  4659  ssrnres  4706  fnun  4948  f1oun  5089  ssimaex  5177  chfnrn  5221  dffo4  5258  dffo5  5259  isoselem  5402  fnoprabg  5544  poxp  5794  issmo2  5845  smores  5848  tfr0  5878  tfrlemibxssdm  5882  swoer  6070  qsss  6101  indpi  6326  recexprlemm  6596  recexprlemloc  6603  recexprlem1ssl  6605  recexprlem1ssu  6606  recexprlemss1l  6607  recexprlemss1u  6608  zmulcl  8073  indstr  8312  eluzdc  8323  icoshft  8628  fzouzsplit  8805  bj-omssind  9394  bj-om  9396  bj-inf2vnlem3  9432  bj-inf2vnlem4  9433