Theorem syl5bi 208

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

Hypotheses

Ref	Expression
syl5bi.1	⊢ (φ ↔ ψ)
syl5bi.2	⊢ (χ → (ψ → θ))

Assertion

Ref	Expression
syl5bi	⊢ (χ → (φ → θ))

Proof of Theorem syl5bi

Step	Hyp	Ref	Expression
1		syl5bi.1	. . 3 ⊢ (φ ↔ ψ)
2	1	biimpi 186	. 2 ⊢ (φ → ψ)
3		syl5bi.2	. 2 ⊢ (χ → (ψ → θ))
4	2, 3	syl5 28	1 ⊢ (χ → (φ → θ))

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  ancomsd  440  3jao  1243  sbequ2  1650  19.9ht  1778  19.9tOLD  1857  ax12olem5  1931  ax11indn  2195  2euex  2276  necon3bd  2554  necon2ad  2565  necon1ad  2584  pm2.61dne  2594  spcimgft  2931  rspc  2950  rspcimdv  2957  euind  3024  reuind  3040  sbciegft  3077  rspsbc  3125  pwpw0  3856  sssn  3865  eqsn  3868  pwsnALT  3883  intss1  3942  intmin  3947  uniintsn  3964  iinss  4018  ssofss  4077  opkth1g  4131  pw1disj  4168  eqpw1uni  4331  nnsucelr  4429  nndisjeq  4430  prepeano4  4452  ltfintr  4460  ssfin  4471  ncfinraise  4482  ncfinlower  4484  nnpw1ex  4485  tfindi  4497  tfinsuc  4499  nnadjoin  4521  nnpweq  4524  sfindbl  4531  tfinnn  4535  sfinltfin  4536  spfininduct  4541  vfintle  4547  vfinspsslem1  4551  vfinspss  4552  nulnnn  4557  phi11lem1  4596  copsexg  4608  iss  5001  xpcan  5058  xpcan2  5059  funssres  5145  funun  5147  funcnvuni  5162  foconst  5281  fun11iun  5306  fv3  5342  fvelima  5370  dff3  5421  fvclss  5463  fununiq  5518  funsi  5521  oprabid  5551  fntxp  5805  fnpprod  5844  weds  5939  erref  5960  erdisj  5973  fundmen  6044  enpw1  6063  enprmaplem3  6079  enprmaplem5  6081  nenpw1pwlem2  6086  ncdisjun  6137  peano4nc  6151  ncssfin  6152  ce0nnulb  6183  fce  6189  addceq0  6220  taddc  6230  letc  6232  addcdi  6251  ncslemuc  6256  addccan2nc  6266  lecadd2  6267  nnc3n3p1  6279  spacis  6289  nchoicelem3  6292  nchoicelem6  6295  nchoicelem9  6298  nchoicelem17  6306  dmfrec  6317  fnfreclem2  6319