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  5652  fvmptt  5728  dff4im  5783  f1eqcocnv  5921  oprabid  6039  f1o2ndf1  6380  poxp  6384  reldmtpos  6405  rntpos  6409  smoiun  6453  tfrlem1  6460  tfrlemi1  6484  tfrexlem  6486  tfri3  6519  nntri3or  6647  qsss  6749  th3qlem1  6792  ixpsnf1o  6891  phplem4  7024  fimax2gtri  7072  fiintim  7104  fisseneq  7107  sbthlemi10  7144  supmoti  7171  suplub2ti  7179  ordiso2  7213  ltmpig  7537  prcdnql  7682  prcunqu  7683  recexprlem1ssl  7831  recexprlem1ssu  7832  recexprlemss1l  7833  recexprlemss1u  7834  cauappcvgprlemladdru  7854  cauappcvgprlemladdrl  7855  caucvgprlemladdrl  7876  mulgt0sr  7976  suplocsrlem  8006  axprecex  8078  ltxrlt  8223  addid0  8530  negf1o  8539  cju  9119  nngt1ne1  9156  nnsub  9160  0mnnnnn0  9412  un0addcl  9413  un0mulcl  9414  zapne  9532  eluzuzle  9742  indstr  9800  elpq  9856  xposdif  10090  ixxdisj  10111  icodisj  10200  uzsubsubfz  10255  elfzmlbp  10340  fzofzim  10400  subfzo0  10460  addmodlteq  10632  seq3f1olemp  10749  seqf1og  10755  expcl2lemap  10785  expnegzap  10807  expaddzap  10817  expmulzap  10819  facwordi  10974  bccl  11001  hashfacen  11071  fundm2domnop0  11080  wrdind  11270  wrd2ind  11271  swrdccatin1  11273  swrdccatin2  11277  pfxccat3  11282  pfxccat3a  11286  swrdccat3blem  11287  reuccatpfxs1  11295  ovshftex  11346  cau3lem  11641  maxabslemval  11735  rexanre  11747  xrmaxiflemval  11777  2clim  11828  summodc  11910  fsum2dlemstep  11961  fsumiun  12004  prodmodc  12105  fprod2dlemstep  12149  odd2np1lem  12399  oddge22np1  12408  sqoddm1div8z  12413  divalglemeunn  12448  divalglemeuneg  12450  bitsfzo  12482  gcd0id  12516  divgcdcoprm0  12639  prmdvdsexpr  12688  prmfac1  12690  qnumdencl  12725  hashdvds  12759  prm23lt5  12802  pcneg  12864  prmpwdvds  12894  ctinf  13017  imasaddfnlemg  13363  mnd1id  13505  0subm  13533  insubm  13534  dfgrp3mlem  13647  ringrng  14015  domnmuln0  14253  lss1d  14363  islidlm  14459  rnglidlmcl  14460  tgcl  14754  epttop  14780  txbas  14948  txbasval  14957  txcnp  14961  txdis1cn  14968  bldisj  15091  reopnap  15236  dvfgg  15378  lgsdir2lem2  15724  gausslemma2dlem1a  15753  gausslemma2dlem3  15758  gausslemma2d  15764  2lgsoddprmlem2  15801  ushgredgedg  16040  ushgredgedgloop  16042  wlk1walkdom  16105  upgriswlkdc  16106  uspgr2wlkeq  16111  bj-vtoclgft  16222  bj-charfun  16253  bj-charfunbi  16257  bj-indind  16378  bj-nntrans  16397  bj-nnelirr  16399  triap  16485