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  871  3jao  1280  19.33b2  1609  sbequ2  1743  sbi1v  1864  mor  2042  2euex  2087  eqneqall  2319  necon3ad  2351  necon1aidc  2360  necon4addc  2379  elnelall  2416  spcimgft  2765  spcimegft  2767  rspc  2787  rspcimdv  2794  rspc2gv  2805  euind  2875  2reuswapdc  2892  reuind  2893  sbciegft  2943  rspsbc  2995  preqr2g  3702  prel12  3706  intss1  3794  intmin  3799  iinss  3872  disjiun  3932  trel3  4042  trin  4044  repizf2  4094  exmidsssnc  4134  copsexg  4174  po3nr  4240  sowlin  4250  eusvnfb  4383  reusv3  4389  ssorduni  4411  ordsucim  4424  tfis2f  4506  ssrelrel  4647  relop  4697  iss  4873  poirr2  4939  funopg  5165  funssres  5173  funun  5175  funcnvuni  5200  fv3  5452  fvmptt  5520  dff4im  5574  f1eqcocnv  5700  oprabid  5811  f1o2ndf1  6133  poxp  6137  reldmtpos  6158  rntpos  6162  smoiun  6206  tfrlem1  6213  tfrlemi1  6237  tfrexlem  6239  tfri3  6272  nntri3or  6397  qsss  6496  th3qlem1  6539  ixpsnf1o  6638  phplem4  6757  fimax2gtri  6803  fiintim  6825  fisseneq  6828  sbthlemi10  6862  supmoti  6888  suplub2ti  6896  ordiso2  6928  ltmpig  7171  prcdnql  7316  prcunqu  7317  recexprlem1ssl  7465  recexprlem1ssu  7466  recexprlemss1l  7467  recexprlemss1u  7468  cauappcvgprlemladdru  7488  cauappcvgprlemladdrl  7489  caucvgprlemladdrl  7510  mulgt0sr  7610  suplocsrlem  7640  axprecex  7712  ltxrlt  7854  addid0  8159  negf1o  8168  cju  8743  nngt1ne1  8779  nnsub  8783  0mnnnnn0  9033  un0addcl  9034  un0mulcl  9035  zapne  9149  eluzuzle  9358  indstr  9415  elpq  9467  xposdif  9695  ixxdisj  9716  icodisj  9805  uzsubsubfz  9858  elfzmlbp  9940  fzofzim  9996  subfzo0  10050  addmodlteq  10202  seq3f1olemp  10306  expcl2lemap  10336  expnegzap  10358  expaddzap  10368  expmulzap  10370  facwordi  10518  bccl  10545  hashfacen  10611  ovshftex  10623  cau3lem  10918  maxabslemval  11012  rexanre  11024  xrmaxiflemval  11051  2clim  11102  summodc  11184  fsum2dlemstep  11235  fsumiun  11278  prodmodc  11379  odd2np1lem  11605  oddge22np1  11614  sqoddm1div8z  11619  divalglemeunn  11654  divalglemeuneg  11656  gcd0id  11703  divgcdcoprm0  11818  prmdvdsexpr  11864  prmfac1  11866  qnumdencl  11901  hashdvds  11933  ctinf  11979  tgcl  12272  epttop  12298  txbas  12466  txbasval  12475  txcnp  12479  txdis1cn  12486  bldisj  12609  reopnap  12746  dvfgg  12865  bj-vtoclgft  13153  bj-indind  13301  bj-nntrans  13320  bj-nnelirr  13322  triap  13399