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  870  3jao  1279  19.33b2  1608  sbequ2  1742  sbi1v  1863  mor  2041  2euex  2086  eqneqall  2318  necon3ad  2350  necon1aidc  2359  necon4addc  2378  elnelall  2415  spcimgft  2762  spcimegft  2764  rspc  2783  rspcimdv  2790  rspc2gv  2801  euind  2871  2reuswapdc  2888  reuind  2889  sbciegft  2939  rspsbc  2991  preqr2g  3694  prel12  3698  intss1  3786  intmin  3791  iinss  3864  disjiun  3924  trel3  4034  trin  4036  repizf2  4086  exmidsssnc  4126  copsexg  4166  po3nr  4232  sowlin  4242  eusvnfb  4375  reusv3  4381  ssorduni  4403  ordsucim  4416  tfis2f  4498  ssrelrel  4639  relop  4689  iss  4865  poirr2  4931  funopg  5157  funssres  5165  funun  5167  funcnvuni  5192  fv3  5444  fvmptt  5512  dff4im  5566  f1eqcocnv  5692  oprabid  5803  f1o2ndf1  6125  poxp  6129  reldmtpos  6150  rntpos  6154  smoiun  6198  tfrlem1  6205  tfrlemi1  6229  tfrexlem  6231  tfri3  6264  nntri3or  6389  qsss  6488  th3qlem1  6531  ixpsnf1o  6630  phplem4  6749  fimax2gtri  6795  fiintim  6817  fisseneq  6820  sbthlemi10  6854  supmoti  6880  suplub2ti  6888  ordiso2  6920  ltmpig  7147  prcdnql  7292  prcunqu  7293  recexprlem1ssl  7441  recexprlem1ssu  7442  recexprlemss1l  7443  recexprlemss1u  7444  cauappcvgprlemladdru  7464  cauappcvgprlemladdrl  7465  caucvgprlemladdrl  7486  mulgt0sr  7586  suplocsrlem  7616  axprecex  7688  ltxrlt  7830  addid0  8135  negf1o  8144  cju  8719  nngt1ne1  8755  nnsub  8759  0mnnnnn0  9009  un0addcl  9010  un0mulcl  9011  zapne  9125  eluzuzle  9334  indstr  9388  xposdif  9665  ixxdisj  9686  icodisj  9775  uzsubsubfz  9827  elfzmlbp  9909  fzofzim  9965  subfzo0  10019  addmodlteq  10171  seq3f1olemp  10275  expcl2lemap  10305  expnegzap  10327  expaddzap  10337  expmulzap  10339  facwordi  10486  bccl  10513  hashfacen  10579  ovshftex  10591  cau3lem  10886  maxabslemval  10980  rexanre  10992  xrmaxiflemval  11019  2clim  11070  summodc  11152  fsum2dlemstep  11203  fsumiun  11246  prodmodc  11347  odd2np1lem  11569  oddge22np1  11578  sqoddm1div8z  11583  divalglemeunn  11618  divalglemeuneg  11620  gcd0id  11667  divgcdcoprm0  11782  prmdvdsexpr  11828  prmfac1  11830  qnumdencl  11865  hashdvds  11897  ctinf  11943  tgcl  12233  epttop  12259  txbas  12427  txbasval  12436  txcnp  12440  txdis1cn  12447  bldisj  12570  reopnap  12707  dvfgg  12826  bj-vtoclgft  12982  bj-indind  13130  bj-nntrans  13149  bj-nnelirr  13151  triap  13224