Theorem syl5bi 151

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 119	. 2 ⊢ (𝜑 → 𝜓)
3		syl5bi.2	. 2 ⊢ (𝜒 → (𝜓 → 𝜃))
4	2, 3	syl5 32	1 ⊢ (𝜒 → (𝜑 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3imtr4g  204  ancomsd  267  pm2.13dc  881  3jao  1297  19.33b2  1623  sbequ2  1763  sbi1v  1885  mor  2062  2euex  2107  eqneqall  2351  necon3ad  2383  necon1aidc  2392  necon4addc  2411  elnelall  2448  spcimgft  2807  spcimegft  2809  rspc  2829  rspcimdv  2836  rspc2gv  2847  euind  2918  2reuswapdc  2935  reuind  2936  sbciegft  2986  rspsbc  3038  preqr2g  3755  prel12  3759  intss1  3847  intmin  3852  iinss  3925  disjiun  3985  trel3  4096  trin  4098  repizf2  4149  exmidsssnc  4190  copsexg  4230  po3nr  4296  sowlin  4306  eusvnfb  4440  reusv3  4446  ssorduni  4472  ordsucim  4485  tfis2f  4569  ssrelrel  4712  relop  4762  iss  4938  poirr2  5005  funopg  5234  funssres  5242  funun  5244  funcnvuni  5269  fv3  5522  fvmptt  5591  dff4im  5646  f1eqcocnv  5774  oprabid  5889  f1o2ndf1  6211  poxp  6215  reldmtpos  6236  rntpos  6240  smoiun  6284  tfrlem1  6291  tfrlemi1  6315  tfrexlem  6317  tfri3  6350  nntri3or  6476  qsss  6576  th3qlem1  6619  ixpsnf1o  6718  phplem4  6837  fimax2gtri  6883  fiintim  6910  fisseneq  6913  sbthlemi10  6947  supmoti  6974  suplub2ti  6982  ordiso2  7016  ltmpig  7305  prcdnql  7450  prcunqu  7451  recexprlem1ssl  7599  recexprlem1ssu  7600  recexprlemss1l  7601  recexprlemss1u  7602  cauappcvgprlemladdru  7622  cauappcvgprlemladdrl  7623  caucvgprlemladdrl  7644  mulgt0sr  7744  suplocsrlem  7774  axprecex  7846  ltxrlt  7989  addid0  8296  negf1o  8305  cju  8881  nngt1ne1  8917  nnsub  8921  0mnnnnn0  9171  un0addcl  9172  un0mulcl  9173  zapne  9290  eluzuzle  9499  indstr  9556  elpq  9611  xposdif  9843  ixxdisj  9864  icodisj  9953  uzsubsubfz  10007  elfzmlbp  10092  fzofzim  10148  subfzo0  10202  addmodlteq  10358  seq3f1olemp  10462  expcl2lemap  10492  expnegzap  10514  expaddzap  10524  expmulzap  10526  facwordi  10678  bccl  10705  hashfacen  10775  ovshftex  10787  cau3lem  11082  maxabslemval  11176  rexanre  11188  xrmaxiflemval  11217  2clim  11268  summodc  11350  fsum2dlemstep  11401  fsumiun  11444  prodmodc  11545  fprod2dlemstep  11589  odd2np1lem  11835  oddge22np1  11844  sqoddm1div8z  11849  divalglemeunn  11884  divalglemeuneg  11886  gcd0id  11938  divgcdcoprm0  12059  prmdvdsexpr  12108  prmfac1  12110  qnumdencl  12145  hashdvds  12179  prm23lt5  12221  pcneg  12282  prmpwdvds  12311  ctinf  12389  mnd1id  12684  0subm  12706  insubm  12707  dfgrp3mlem  12801  tgcl  12943  epttop  12969  txbas  13137  txbasval  13146  txcnp  13150  txdis1cn  13157  bldisj  13280  reopnap  13417  dvfgg  13536  lgsdir2lem2  13809  bj-vtoclgft  13895  bj-charfun  13927  bj-charfunbi  13931  bj-indind  14052  bj-nntrans  14071  bj-nnelirr  14073  triap  14146