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  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  3754  prel12  3758  intss1  3846  intmin  3851  iinss  3924  disjiun  3984  trel3  4095  trin  4097  repizf2  4148  exmidsssnc  4189  copsexg  4229  po3nr  4295  sowlin  4305  eusvnfb  4439  reusv3  4445  ssorduni  4471  ordsucim  4484  tfis2f  4568  ssrelrel  4711  relop  4761  iss  4937  poirr2  5003  funopg  5232  funssres  5240  funun  5242  funcnvuni  5267  fv3  5519  fvmptt  5587  dff4im  5642  f1eqcocnv  5770  oprabid  5885  f1o2ndf1  6207  poxp  6211  reldmtpos  6232  rntpos  6236  smoiun  6280  tfrlem1  6287  tfrlemi1  6311  tfrexlem  6313  tfri3  6346  nntri3or  6472  qsss  6572  th3qlem1  6615  ixpsnf1o  6714  phplem4  6833  fimax2gtri  6879  fiintim  6906  fisseneq  6909  sbthlemi10  6943  supmoti  6970  suplub2ti  6978  ordiso2  7012  ltmpig  7301  prcdnql  7446  prcunqu  7447  recexprlem1ssl  7595  recexprlem1ssu  7596  recexprlemss1l  7597  recexprlemss1u  7598  cauappcvgprlemladdru  7618  cauappcvgprlemladdrl  7619  caucvgprlemladdrl  7640  mulgt0sr  7740  suplocsrlem  7770  axprecex  7842  ltxrlt  7985  addid0  8292  negf1o  8301  cju  8877  nngt1ne1  8913  nnsub  8917  0mnnnnn0  9167  un0addcl  9168  un0mulcl  9169  zapne  9286  eluzuzle  9495  indstr  9552  elpq  9607  xposdif  9839  ixxdisj  9860  icodisj  9949  uzsubsubfz  10003  elfzmlbp  10088  fzofzim  10144  subfzo0  10198  addmodlteq  10354  seq3f1olemp  10458  expcl2lemap  10488  expnegzap  10510  expaddzap  10520  expmulzap  10522  facwordi  10674  bccl  10701  hashfacen  10771  ovshftex  10783  cau3lem  11078  maxabslemval  11172  rexanre  11184  xrmaxiflemval  11213  2clim  11264  summodc  11346  fsum2dlemstep  11397  fsumiun  11440  prodmodc  11541  fprod2dlemstep  11585  odd2np1lem  11831  oddge22np1  11840  sqoddm1div8z  11845  divalglemeunn  11880  divalglemeuneg  11882  gcd0id  11934  divgcdcoprm0  12055  prmdvdsexpr  12104  prmfac1  12106  qnumdencl  12141  hashdvds  12175  prm23lt5  12217  pcneg  12278  prmpwdvds  12307  ctinf  12385  mnd1id  12680  0subm  12702  insubm  12703  tgcl  12858  epttop  12884  txbas  13052  txbasval  13061  txcnp  13065  txdis1cn  13072  bldisj  13195  reopnap  13332  dvfgg  13451  lgsdir2lem2  13724  bj-vtoclgft  13810  bj-charfun  13842  bj-charfunbi  13846  bj-indind  13967  bj-nntrans  13986  bj-nnelirr  13988  triap  14061