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  1640  sbequ2  1780  sbi1v  1903  mor  2084  2euex  2129  eqneqall  2374  necon3ad  2406  necon1aidc  2415  necon4addc  2434  elnelall  2471  spcimgft  2837  spcimegft  2839  rspc  2859  rspcimdv  2866  rspc2gv  2877  euind  2948  2reuswapdc  2965  reuind  2966  sbciegft  3017  rspsbc  3069  preqr2g  3794  prel12  3798  intss1  3886  intmin  3891  iinss  3965  disjiun  4025  trel3  4136  trin  4138  repizf2  4192  exmidsssnc  4233  copsexg  4274  po3nr  4342  sowlin  4352  eusvnfb  4486  reusv3  4492  ssorduni  4520  ordsucim  4533  tfis2f  4617  ssrelrel  4760  relop  4813  iss  4989  poirr2  5059  funopg  5289  funssres  5297  funun  5299  funcnvuni  5324  fv3  5578  fvmptt  5650  dff4im  5705  f1eqcocnv  5835  oprabid  5951  f1o2ndf1  6283  poxp  6287  reldmtpos  6308  rntpos  6312  smoiun  6356  tfrlem1  6363  tfrlemi1  6387  tfrexlem  6389  tfri3  6422  nntri3or  6548  qsss  6650  th3qlem1  6693  ixpsnf1o  6792  phplem4  6913  fimax2gtri  6959  fiintim  6987  fisseneq  6990  sbthlemi10  7027  supmoti  7054  suplub2ti  7062  ordiso2  7096  ltmpig  7401  prcdnql  7546  prcunqu  7547  recexprlem1ssl  7695  recexprlem1ssu  7696  recexprlemss1l  7697  recexprlemss1u  7698  cauappcvgprlemladdru  7718  cauappcvgprlemladdrl  7719  caucvgprlemladdrl  7740  mulgt0sr  7840  suplocsrlem  7870  axprecex  7942  ltxrlt  8087  addid0  8394  negf1o  8403  cju  8982  nngt1ne1  9019  nnsub  9023  0mnnnnn0  9275  un0addcl  9276  un0mulcl  9277  zapne  9394  eluzuzle  9603  indstr  9661  elpq  9717  xposdif  9951  ixxdisj  9972  icodisj  10061  uzsubsubfz  10116  elfzmlbp  10201  fzofzim  10258  subfzo0  10312  addmodlteq  10472  seq3f1olemp  10589  seqf1og  10595  expcl2lemap  10625  expnegzap  10647  expaddzap  10657  expmulzap  10659  facwordi  10814  bccl  10841  hashfacen  10910  ovshftex  10966  cau3lem  11261  maxabslemval  11355  rexanre  11367  xrmaxiflemval  11396  2clim  11447  summodc  11529  fsum2dlemstep  11580  fsumiun  11623  prodmodc  11724  fprod2dlemstep  11768  odd2np1lem  12016  oddge22np1  12025  sqoddm1div8z  12030  divalglemeunn  12065  divalglemeuneg  12067  gcd0id  12119  divgcdcoprm0  12242  prmdvdsexpr  12291  prmfac1  12293  qnumdencl  12328  hashdvds  12362  prm23lt5  12404  pcneg  12466  prmpwdvds  12496  ctinf  12590  imasaddfnlemg  12900  mnd1id  13031  0subm  13059  insubm  13060  dfgrp3mlem  13173  ringrng  13535  domnmuln0  13772  lss1d  13882  islidlm  13978  rnglidlmcl  13979  tgcl  14243  epttop  14269  txbas  14437  txbasval  14446  txcnp  14450  txdis1cn  14457  bldisj  14580  reopnap  14725  dvfgg  14867  lgsdir2lem2  15186  gausslemma2dlem1a  15215  gausslemma2dlem3  15220  gausslemma2d  15226  2lgsoddprmlem2  15263  bj-vtoclgft  15337  bj-charfun  15369  bj-charfunbi  15373  bj-indind  15494  bj-nntrans  15513  bj-nnelirr  15515  triap  15589