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	|- ( ph <-> ps )
syl5bi.2	|- ( ch -> ( ps -> th ) )

Assertion

Ref	Expression
syl5bi	|- ( ch -> ( ph -> th ) )

Proof of Theorem syl5bi

Step	Hyp	Ref	Expression
1		syl5bi.1	. . 3 |- ( ph <-> ps )
2	1	biimpi 119	. 2 |- ( ph -> ps )
3		syl5bi.2	. 2 |- ( ch -> ( ps -> th ) )
4	2, 3	syl5 32	1 |- ( ch -> ( ph -> th ) )

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  1283  19.33b2  1609  sbequ2  1749  sbi1v  1871  mor  2048  2euex  2093  eqneqall  2337  necon3ad  2369  necon1aidc  2378  necon4addc  2397  elnelall  2434  spcimgft  2788  spcimegft  2790  rspc  2810  rspcimdv  2817  rspc2gv  2828  euind  2899  2reuswapdc  2916  reuind  2917  sbciegft  2967  rspsbc  3019  preqr2g  3730  prel12  3734  intss1  3822  intmin  3827  iinss  3900  disjiun  3960  trel3  4070  trin  4072  repizf2  4123  exmidsssnc  4164  copsexg  4204  po3nr  4270  sowlin  4280  eusvnfb  4414  reusv3  4420  ssorduni  4446  ordsucim  4459  tfis2f  4543  ssrelrel  4686  relop  4736  iss  4912  poirr2  4978  funopg  5204  funssres  5212  funun  5214  funcnvuni  5239  fv3  5491  fvmptt  5559  dff4im  5613  f1eqcocnv  5741  oprabid  5853  f1o2ndf1  6175  poxp  6179  reldmtpos  6200  rntpos  6204  smoiun  6248  tfrlem1  6255  tfrlemi1  6279  tfrexlem  6281  tfri3  6314  nntri3or  6440  qsss  6539  th3qlem1  6582  ixpsnf1o  6681  phplem4  6800  fimax2gtri  6846  fiintim  6873  fisseneq  6876  sbthlemi10  6910  supmoti  6937  suplub2ti  6945  ordiso2  6979  ltmpig  7259  prcdnql  7404  prcunqu  7405  recexprlem1ssl  7553  recexprlem1ssu  7554  recexprlemss1l  7555  recexprlemss1u  7556  cauappcvgprlemladdru  7576  cauappcvgprlemladdrl  7577  caucvgprlemladdrl  7598  mulgt0sr  7698  suplocsrlem  7728  axprecex  7800  ltxrlt  7943  addid0  8248  negf1o  8257  cju  8832  nngt1ne1  8868  nnsub  8872  0mnnnnn0  9122  un0addcl  9123  un0mulcl  9124  zapne  9238  eluzuzle  9447  indstr  9504  elpq  9557  xposdif  9786  ixxdisj  9807  icodisj  9896  uzsubsubfz  9949  elfzmlbp  10031  fzofzim  10087  subfzo0  10141  addmodlteq  10297  seq3f1olemp  10401  expcl2lemap  10431  expnegzap  10453  expaddzap  10463  expmulzap  10465  facwordi  10614  bccl  10641  hashfacen  10707  ovshftex  10719  cau3lem  11014  maxabslemval  11108  rexanre  11120  xrmaxiflemval  11147  2clim  11198  summodc  11280  fsum2dlemstep  11331  fsumiun  11374  prodmodc  11475  fprod2dlemstep  11519  odd2np1lem  11762  oddge22np1  11771  sqoddm1div8z  11776  divalglemeunn  11811  divalglemeuneg  11813  gcd0id  11862  divgcdcoprm0  11977  prmdvdsexpr  12024  prmfac1  12026  qnumdencl  12061  hashdvds  12095  ctinf  12159  tgcl  12464  epttop  12490  txbas  12658  txbasval  12667  txcnp  12671  txdis1cn  12678  bldisj  12801  reopnap  12938  dvfgg  13057  bj-vtoclgft  13349  bj-charfun  13382  bj-charfunbi  13386  bj-indind  13507  bj-nntrans  13526  bj-nnelirr  13528  triap  13600