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  2553  necon2ad  2564  necon1ad  2583  pm2.61dne  2593  spcimgft  2930  rspc  2949  rspcimdv  2956  euind  3023  reuind  3039  sbciegft  3076  rspsbc  3124  pwpw0  3855  sssn  3864  eqsn  3867  pwsnALT  3882  intss1  3941  intmin  3946  uniintsn  3963  iinss  4017  ssofss  4076  opkth1g  4130  pw1disj  4167  eqpw1uni  4330  nnsucelr  4428  nndisjeq  4429  prepeano4  4451  ltfintr  4459  ssfin  4470  ncfinraise  4481  ncfinlower  4483  nnpw1ex  4484  tfindi  4496  tfinsuc  4498  nnadjoin  4520  nnpweq  4523  sfindbl  4530  tfinnn  4534  sfinltfin  4535  spfininduct  4540  vfintle  4546  vfinspsslem1  4550  vfinspss  4551  nulnnn  4556  phi11lem1  4595  copsexg  4607  iss  5000  xpcan  5057  xpcan2  5058  funssres  5144  funun  5146  funcnvuni  5161  foconst  5280  fun11iun  5305  fv3  5341  fvelima  5369  dff3  5420  fvclss  5462  fununiq  5517  funsi  5520  oprabid  5550  fntxp  5804  fnpprod  5843  weds  5938  erref  5959  erdisj  5972  fundmen  6043  enpw1  6062  enprmaplem3  6078  enprmaplem5  6080  nenpw1pwlem2  6085  ncdisjun  6136  peano4nc  6150  ncssfin  6151  ce0nnulb  6182  fce  6188  addceq0  6219  taddc  6229  letc  6231  addcdi  6250  ncslemuc  6255  addccan2nc  6265  lecadd2  6266  nnc3n3p1  6278  spacis  6288  nchoicelem3  6291  nchoicelem6  6294  nchoicelem9  6297  nchoicelem17  6305  dmfrec  6316  fnfreclem2  6318