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  887  3jao  1314  19.33b2  1652  sbequ2  1792  sbi1v  1915  mor  2096  2euex  2141  eqneqall  2386  necon3ad  2418  necon1aidc  2427  necon4addc  2446  elnelall  2483  spcimgft  2849  spcimegft  2851  rspc  2871  rspcimdv  2878  rspc2gv  2889  euind  2960  2reuswapdc  2977  reuind  2978  sbciegft  3029  rspsbc  3081  preqr2g  3808  prel12  3812  intss1  3900  intmin  3905  iinss  3979  disjiun  4040  trel3  4151  trin  4153  repizf2  4207  exmidsssnc  4248  copsexg  4289  po3nr  4358  sowlin  4368  eusvnfb  4502  reusv3  4508  ssorduni  4536  ordsucim  4549  tfis2f  4633  ssrelrel  4776  relop  4829  iss  5006  poirr2  5076  funopg  5306  funssres  5314  funun  5316  funcnvuni  5344  fv3  5601  fvmptt  5673  dff4im  5728  f1eqcocnv  5862  oprabid  5978  f1o2ndf1  6316  poxp  6320  reldmtpos  6341  rntpos  6345  smoiun  6389  tfrlem1  6396  tfrlemi1  6420  tfrexlem  6422  tfri3  6455  nntri3or  6581  qsss  6683  th3qlem1  6726  ixpsnf1o  6825  phplem4  6954  fimax2gtri  7000  fiintim  7030  fisseneq  7033  sbthlemi10  7070  supmoti  7097  suplub2ti  7105  ordiso2  7139  ltmpig  7454  prcdnql  7599  prcunqu  7600  recexprlem1ssl  7748  recexprlem1ssu  7749  recexprlemss1l  7750  recexprlemss1u  7751  cauappcvgprlemladdru  7771  cauappcvgprlemladdrl  7772  caucvgprlemladdrl  7793  mulgt0sr  7893  suplocsrlem  7923  axprecex  7995  ltxrlt  8140  addid0  8447  negf1o  8456  cju  9036  nngt1ne1  9073  nnsub  9077  0mnnnnn0  9329  un0addcl  9330  un0mulcl  9331  zapne  9449  eluzuzle  9658  indstr  9716  elpq  9772  xposdif  10006  ixxdisj  10027  icodisj  10116  uzsubsubfz  10171  elfzmlbp  10256  fzofzim  10314  subfzo0  10373  addmodlteq  10545  seq3f1olemp  10662  seqf1og  10668  expcl2lemap  10698  expnegzap  10720  expaddzap  10730  expmulzap  10732  facwordi  10887  bccl  10914  hashfacen  10983  fundm2domnop0  10992  ovshftex  11163  cau3lem  11458  maxabslemval  11552  rexanre  11564  xrmaxiflemval  11594  2clim  11645  summodc  11727  fsum2dlemstep  11778  fsumiun  11821  prodmodc  11922  fprod2dlemstep  11966  odd2np1lem  12216  oddge22np1  12225  sqoddm1div8z  12230  divalglemeunn  12265  divalglemeuneg  12267  bitsfzo  12299  gcd0id  12333  divgcdcoprm0  12456  prmdvdsexpr  12505  prmfac1  12507  qnumdencl  12542  hashdvds  12576  prm23lt5  12619  pcneg  12681  prmpwdvds  12711  ctinf  12834  imasaddfnlemg  13179  mnd1id  13321  0subm  13349  insubm  13350  dfgrp3mlem  13463  ringrng  13831  domnmuln0  14068  lss1d  14178  islidlm  14274  rnglidlmcl  14275  tgcl  14569  epttop  14595  txbas  14763  txbasval  14772  txcnp  14776  txdis1cn  14783  bldisj  14906  reopnap  15051  dvfgg  15193  lgsdir2lem2  15539  gausslemma2dlem1a  15568  gausslemma2dlem3  15573  gausslemma2d  15579  2lgsoddprmlem2  15616  bj-vtoclgft  15748  bj-charfun  15780  bj-charfunbi  15784  bj-indind  15905  bj-nntrans  15924  bj-nnelirr  15926  triap  16005