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  886  3jao  1312  19.33b2  1643  sbequ2  1783  sbi1v  1906  mor  2087  2euex  2132  eqneqall  2377  necon3ad  2409  necon1aidc  2418  necon4addc  2437  elnelall  2474  spcimgft  2840  spcimegft  2842  rspc  2862  rspcimdv  2869  rspc2gv  2880  euind  2951  2reuswapdc  2968  reuind  2969  sbciegft  3020  rspsbc  3072  preqr2g  3798  prel12  3802  intss1  3890  intmin  3895  iinss  3969  disjiun  4029  trel3  4140  trin  4142  repizf2  4196  exmidsssnc  4237  copsexg  4278  po3nr  4346  sowlin  4356  eusvnfb  4490  reusv3  4496  ssorduni  4524  ordsucim  4537  tfis2f  4621  ssrelrel  4764  relop  4817  iss  4993  poirr2  5063  funopg  5293  funssres  5301  funun  5303  funcnvuni  5328  fv3  5584  fvmptt  5656  dff4im  5711  f1eqcocnv  5841  oprabid  5957  f1o2ndf1  6295  poxp  6299  reldmtpos  6320  rntpos  6324  smoiun  6368  tfrlem1  6375  tfrlemi1  6399  tfrexlem  6401  tfri3  6434  nntri3or  6560  qsss  6662  th3qlem1  6705  ixpsnf1o  6804  phplem4  6925  fimax2gtri  6971  fiintim  7001  fisseneq  7004  sbthlemi10  7041  supmoti  7068  suplub2ti  7076  ordiso2  7110  ltmpig  7423  prcdnql  7568  prcunqu  7569  recexprlem1ssl  7717  recexprlem1ssu  7718  recexprlemss1l  7719  recexprlemss1u  7720  cauappcvgprlemladdru  7740  cauappcvgprlemladdrl  7741  caucvgprlemladdrl  7762  mulgt0sr  7862  suplocsrlem  7892  axprecex  7964  ltxrlt  8109  addid0  8416  negf1o  8425  cju  9005  nngt1ne1  9042  nnsub  9046  0mnnnnn0  9298  un0addcl  9299  un0mulcl  9300  zapne  9417  eluzuzle  9626  indstr  9684  elpq  9740  xposdif  9974  ixxdisj  9995  icodisj  10084  uzsubsubfz  10139  elfzmlbp  10224  fzofzim  10281  subfzo0  10335  addmodlteq  10507  seq3f1olemp  10624  seqf1og  10630  expcl2lemap  10660  expnegzap  10682  expaddzap  10692  expmulzap  10694  facwordi  10849  bccl  10876  hashfacen  10945  ovshftex  11001  cau3lem  11296  maxabslemval  11390  rexanre  11402  xrmaxiflemval  11432  2clim  11483  summodc  11565  fsum2dlemstep  11616  fsumiun  11659  prodmodc  11760  fprod2dlemstep  11804  odd2np1lem  12054  oddge22np1  12063  sqoddm1div8z  12068  divalglemeunn  12103  divalglemeuneg  12105  bitsfzo  12137  gcd0id  12171  divgcdcoprm0  12294  prmdvdsexpr  12343  prmfac1  12345  qnumdencl  12380  hashdvds  12414  prm23lt5  12457  pcneg  12519  prmpwdvds  12549  ctinf  12672  imasaddfnlemg  13016  mnd1id  13158  0subm  13186  insubm  13187  dfgrp3mlem  13300  ringrng  13668  domnmuln0  13905  lss1d  14015  islidlm  14111  rnglidlmcl  14112  tgcl  14384  epttop  14410  txbas  14578  txbasval  14587  txcnp  14591  txdis1cn  14598  bldisj  14721  reopnap  14866  dvfgg  15008  lgsdir2lem2  15354  gausslemma2dlem1a  15383  gausslemma2dlem3  15388  gausslemma2d  15394  2lgsoddprmlem2  15431  bj-vtoclgft  15505  bj-charfun  15537  bj-charfunbi  15541  bj-indind  15662  bj-nntrans  15681  bj-nnelirr  15683  triap  15760