Theorem syl5bi 150

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 118	. 2 |- ( ph -> ps )
3		syl5bi.2	. 2 |- ( ch -> ( ps -> th ) )
4	2, 3	syl5 32	1 |- ( ch -> ( ph -> th ) )

Syntax hints:   -> wi 4   <-> wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  3imtr4g  203  ancomsd  265  pm2.13dc  812  3jao  1232  19.33b2  1560  sbequ2  1692  sbi1v  1812  mor  1983  2euex  2028  eqneqall  2255  necon3ad  2287  necon1aidc  2296  necon4addc  2315  spcimgft  2674  spcimegft  2676  rspc  2695  rspcimdv  2702  rspc2gv  2712  euind  2779  2reuswapdc  2794  reuind  2795  sbciegft  2844  rspsbc  2896  preqr2g  3559  prel12  3563  intss1  3651  intmin  3656  iinss  3729  trel3  3883  trin  3885  trintssmOLD  3892  repizf2  3936  copsexg  3999  po3nr  4065  sowlin  4075  eusvnfb  4204  reusv3  4210  ssorduni  4231  ordsucim  4244  tfis2f  4325  ssrelrel  4458  relop  4504  iss  4674  poirr2  4737  funopg  4954  funssres  4962  funun  4964  funcnvuni  4988  fv3  5218  fvmptt  5283  dff4im  5334  f1eqcocnv  5451  oprabid  5557  f1o2ndf1  5869  poxp  5873  reldmtpos  5891  rntpos  5895  smoiun  5939  tfrlem1  5946  tfrlemi1  5969  tfrexlem  5971  tfri3  5976  rdgon  5996  nntri3or  6095  qsss  6188  th3qlem1  6231  phplem4  6341  supmoti  6406  suplub2ti  6414  ordiso2  6446  ltmpig  6529  prcdnql  6674  prcunqu  6675  recexprlem1ssl  6823  recexprlem1ssu  6824  recexprlemss1l  6825  recexprlemss1u  6826  cauappcvgprlemladdru  6846  cauappcvgprlemladdrl  6847  caucvgprlemladdrl  6868  mulgt0sr  6954  axprecex  7046  ltxrlt  7178  addid0  7477  negf1o  7486  cju  8038  nngt1ne1  8073  nnsub  8077  0mnnnnn0  8320  un0addcl  8321  un0mulcl  8322  zapne  8422  eluzuzle  8627  indstr  8681  ixxdisj  8926  icodisj  9014  uzsubsubfz  9066  elfzmlbp  9143  fzofzim  9197  subfzo0  9251  addmodlteq  9400  expcl2lemap  9488  expnegzap  9510  expaddzap  9520  expmulzap  9522  facwordi  9667  bccl  9694  ovshftex  9707  cau3lem  10000  maxabslemval  10094  rexanre  10106  2clim  10140  odd2np1lem  10271  oddge22np1  10281  sqoddm1div8z  10286  divalglemeunn  10321  divalglemeuneg  10323  gcd0id  10370  divgcdcoprm0  10483  prmdvdsexpr  10529  prmfac1  10531  bj-vtoclgft  10585  bj-indind  10727  bj-nntrans  10746  bj-nnelirr  10748