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-1 5  ax-2 6  ax-mp 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3imtr4g  204  ancomsd  266  pm2.13dc  820  3jao  1244  19.33b2  1572  sbequ2  1706  sbi1v  1826  mor  1997  2euex  2042  eqneqall  2272  necon3ad  2304  necon1aidc  2313  necon4addc  2332  elnelall  2369  spcimgft  2709  spcimegft  2711  rspc  2730  rspcimdv  2737  rspc2gv  2747  euind  2816  2reuswapdc  2833  reuind  2834  sbciegft  2883  rspsbc  2935  preqr2g  3633  prel12  3637  intss1  3725  intmin  3730  iinss  3803  disjiun  3862  trel3  3966  trin  3968  repizf2  4018  copsexg  4095  po3nr  4161  sowlin  4171  eusvnfb  4304  reusv3  4310  ssorduni  4332  ordsucim  4345  tfis2f  4427  ssrelrel  4567  relop  4617  iss  4791  poirr2  4857  funopg  5082  funssres  5090  funun  5092  funcnvuni  5117  fv3  5363  fvmptt  5430  dff4im  5484  f1eqcocnv  5608  oprabid  5719  f1o2ndf1  6031  poxp  6035  reldmtpos  6056  rntpos  6060  smoiun  6104  tfrlem1  6111  tfrlemi1  6135  tfrexlem  6137  tfri3  6170  nntri3or  6294  qsss  6391  th3qlem1  6434  ixpsnf1o  6533  phplem4  6651  fimax2gtri  6697  fiintim  6719  fisseneq  6722  sbthlemi10  6755  supmoti  6768  suplub2ti  6776  ordiso2  6808  ltmpig  6995  prcdnql  7140  prcunqu  7141  recexprlem1ssl  7289  recexprlem1ssu  7290  recexprlemss1l  7291  recexprlemss1u  7292  cauappcvgprlemladdru  7312  cauappcvgprlemladdrl  7313  caucvgprlemladdrl  7334  mulgt0sr  7420  axprecex  7512  ltxrlt  7649  addid0  7948  negf1o  7957  cju  8519  nngt1ne1  8555  nnsub  8559  0mnnnnn0  8803  un0addcl  8804  un0mulcl  8805  zapne  8919  eluzuzle  9126  indstr  9180  xposdif  9448  ixxdisj  9469  icodisj  9558  uzsubsubfz  9610  elfzmlbp  9692  fzofzim  9748  subfzo0  9802  addmodlteq  9954  seq3f1olemp  10052  expcl2lemap  10082  expnegzap  10104  expaddzap  10114  expmulzap  10116  facwordi  10263  bccl  10290  hashfacen  10356  ovshftex  10368  cau3lem  10662  maxabslemval  10756  rexanre  10768  xrmaxiflemval  10793  2clim  10844  summodc  10926  fsum2dlemstep  10977  fsumiun  11020  odd2np1lem  11299  oddge22np1  11308  sqoddm1div8z  11313  divalglemeunn  11348  divalglemeuneg  11350  gcd0id  11397  divgcdcoprm0  11510  prmdvdsexpr  11556  prmfac1  11558  qnumdencl  11592  hashdvds  11624  tgcl  11916  epttop  11942  bldisj  12187  bj-vtoclgft  12383  bj-indind  12535  bj-nntrans  12554  bj-nnelirr  12556