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  880  3jao  1296  19.33b2  1622  sbequ2  1762  sbi1v  1884  mor  2061  2euex  2106  eqneqall  2350  necon3ad  2382  necon1aidc  2391  necon4addc  2410  elnelall  2447  spcimgft  2806  spcimegft  2808  rspc  2828  rspcimdv  2835  rspc2gv  2846  euind  2917  2reuswapdc  2934  reuind  2935  sbciegft  2985  rspsbc  3037  preqr2g  3752  prel12  3756  intss1  3844  intmin  3849  iinss  3922  disjiun  3982  trel3  4093  trin  4095  repizf2  4146  exmidsssnc  4187  copsexg  4227  po3nr  4293  sowlin  4303  eusvnfb  4437  reusv3  4443  ssorduni  4469  ordsucim  4482  tfis2f  4566  ssrelrel  4709  relop  4759  iss  4935  poirr2  5001  funopg  5230  funssres  5238  funun  5240  funcnvuni  5265  fv3  5517  fvmptt  5585  dff4im  5639  f1eqcocnv  5767  oprabid  5882  f1o2ndf1  6204  poxp  6208  reldmtpos  6229  rntpos  6233  smoiun  6277  tfrlem1  6284  tfrlemi1  6308  tfrexlem  6310  tfri3  6343  nntri3or  6469  qsss  6568  th3qlem1  6611  ixpsnf1o  6710  phplem4  6829  fimax2gtri  6875  fiintim  6902  fisseneq  6905  sbthlemi10  6939  supmoti  6966  suplub2ti  6974  ordiso2  7008  ltmpig  7288  prcdnql  7433  prcunqu  7434  recexprlem1ssl  7582  recexprlem1ssu  7583  recexprlemss1l  7584  recexprlemss1u  7585  cauappcvgprlemladdru  7605  cauappcvgprlemladdrl  7606  caucvgprlemladdrl  7627  mulgt0sr  7727  suplocsrlem  7757  axprecex  7829  ltxrlt  7972  addid0  8279  negf1o  8288  cju  8864  nngt1ne1  8900  nnsub  8904  0mnnnnn0  9154  un0addcl  9155  un0mulcl  9156  zapne  9273  eluzuzle  9482  indstr  9539  elpq  9594  xposdif  9826  ixxdisj  9847  icodisj  9936  uzsubsubfz  9990  elfzmlbp  10075  fzofzim  10131  subfzo0  10185  addmodlteq  10341  seq3f1olemp  10445  expcl2lemap  10475  expnegzap  10497  expaddzap  10507  expmulzap  10509  facwordi  10661  bccl  10688  hashfacen  10758  ovshftex  10770  cau3lem  11065  maxabslemval  11159  rexanre  11171  xrmaxiflemval  11200  2clim  11251  summodc  11333  fsum2dlemstep  11384  fsumiun  11427  prodmodc  11528  fprod2dlemstep  11572  odd2np1lem  11818  oddge22np1  11827  sqoddm1div8z  11832  divalglemeunn  11867  divalglemeuneg  11869  gcd0id  11921  divgcdcoprm0  12042  prmdvdsexpr  12091  prmfac1  12093  qnumdencl  12128  hashdvds  12162  prm23lt5  12204  pcneg  12265  prmpwdvds  12294  ctinf  12372  mnd1id  12666  0subm  12688  insubm  12689  tgcl  12779  epttop  12805  txbas  12973  txbasval  12982  txcnp  12986  txdis1cn  12993  bldisj  13116  reopnap  13253  dvfgg  13372  lgsdir2lem2  13645  bj-vtoclgft  13731  bj-charfun  13764  bj-charfunbi  13768  bj-indind  13889  bj-nntrans  13908  bj-nnelirr  13910  triap  13983