Theorem biimtrid 152

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

Assertion

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

Proof of Theorem biimtrid

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

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3imtr4g  205  ancomsd  269  pm2.13dc  890  3jao  1335  19.33b2  1675  sbequ2  1815  sbi1v  1938  mor  2120  2euex  2165  eqneqall  2410  necon3ad  2442  necon1aidc  2451  necon4addc  2470  elnelall  2507  spcimgft  2879  spcimegft  2881  rspc  2901  rspcimdv  2908  rspc2gv  2919  euind  2990  2reuswapdc  3007  reuind  3008  sbciegft  3059  rspsbc  3112  preqr2g  3845  prel12  3849  intss1  3938  intmin  3943  iinss  4017  disjiun  4078  trel3  4190  trin  4192  repizf2  4246  exmidsssnc  4287  copsexg  4330  po3nr  4401  sowlin  4411  eusvnfb  4545  reusv3  4551  ssorduni  4579  ordsucim  4592  tfis2f  4676  ssrelrel  4819  relop  4872  iss  5051  poirr2  5121  funopg  5352  funssres  5360  funun  5362  funcnvuni  5390  fv3  5650  fvmptt  5726  dff4im  5781  f1eqcocnv  5915  oprabid  6033  f1o2ndf1  6374  poxp  6378  reldmtpos  6399  rntpos  6403  smoiun  6447  tfrlem1  6454  tfrlemi1  6478  tfrexlem  6480  tfri3  6513  nntri3or  6639  qsss  6741  th3qlem1  6784  ixpsnf1o  6883  phplem4  7016  fimax2gtri  7063  fiintim  7093  fisseneq  7096  sbthlemi10  7133  supmoti  7160  suplub2ti  7168  ordiso2  7202  ltmpig  7526  prcdnql  7671  prcunqu  7672  recexprlem1ssl  7820  recexprlem1ssu  7821  recexprlemss1l  7822  recexprlemss1u  7823  cauappcvgprlemladdru  7843  cauappcvgprlemladdrl  7844  caucvgprlemladdrl  7865  mulgt0sr  7965  suplocsrlem  7995  axprecex  8067  ltxrlt  8212  addid0  8519  negf1o  8528  cju  9108  nngt1ne1  9145  nnsub  9149  0mnnnnn0  9401  un0addcl  9402  un0mulcl  9403  zapne  9521  eluzuzle  9730  indstr  9788  elpq  9844  xposdif  10078  ixxdisj  10099  icodisj  10188  uzsubsubfz  10243  elfzmlbp  10328  fzofzim  10388  subfzo0  10448  addmodlteq  10620  seq3f1olemp  10737  seqf1og  10743  expcl2lemap  10773  expnegzap  10795  expaddzap  10805  expmulzap  10807  facwordi  10962  bccl  10989  hashfacen  11058  fundm2domnop0  11067  wrdind  11254  wrd2ind  11255  swrdccatin1  11257  swrdccatin2  11261  pfxccat3  11266  pfxccat3a  11270  swrdccat3blem  11271  reuccatpfxs1  11279  ovshftex  11330  cau3lem  11625  maxabslemval  11719  rexanre  11731  xrmaxiflemval  11761  2clim  11812  summodc  11894  fsum2dlemstep  11945  fsumiun  11988  prodmodc  12089  fprod2dlemstep  12133  odd2np1lem  12383  oddge22np1  12392  sqoddm1div8z  12397  divalglemeunn  12432  divalglemeuneg  12434  bitsfzo  12466  gcd0id  12500  divgcdcoprm0  12623  prmdvdsexpr  12672  prmfac1  12674  qnumdencl  12709  hashdvds  12743  prm23lt5  12786  pcneg  12848  prmpwdvds  12878  ctinf  13001  imasaddfnlemg  13347  mnd1id  13489  0subm  13517  insubm  13518  dfgrp3mlem  13631  ringrng  13999  domnmuln0  14237  lss1d  14347  islidlm  14443  rnglidlmcl  14444  tgcl  14738  epttop  14764  txbas  14932  txbasval  14941  txcnp  14945  txdis1cn  14952  bldisj  15075  reopnap  15220  dvfgg  15362  lgsdir2lem2  15708  gausslemma2dlem1a  15737  gausslemma2dlem3  15742  gausslemma2d  15748  2lgsoddprmlem2  15785  ushgredgedg  16024  ushgredgedgloop  16026  wlk1walkdom  16070  upgriswlkdc  16071  uspgr2wlkeq  16076  bj-vtoclgft  16139  bj-charfun  16170  bj-charfunbi  16174  bj-indind  16295  bj-nntrans  16314  bj-nnelirr  16316  triap  16397