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  893  3jao  1338  19.33b2  1678  sbequ2  1818  sbi1v  1941  mor  2123  2euex  2168  eqneqall  2422  necon3ad  2454  necon1aidc  2463  necon4addc  2482  elnelall  2519  spcimgft  2893  spcimegft  2895  rspc  2915  rspcimdv  2922  rspc2gv  2933  euind  3004  2reuswapdc  3021  reuind  3022  sbciegft  3073  rspsbc  3126  preqr2g  3871  prel12  3875  intss1  3964  intmin  3969  iinss  4043  disjiun  4104  trel3  4216  trin  4218  repizf2  4275  exmidsssnc  4316  copsexg  4360  po3nr  4431  sowlin  4441  eusvnfb  4575  reusv3  4581  ssorduni  4609  ordsucim  4622  tfis2f  4706  ssrelrel  4850  relop  4905  iss  5084  poirr2  5155  funopg  5386  funssres  5395  funun  5397  funcnvuni  5425  fv3  5693  fvmptt  5769  dff4im  5823  f1eqcocnv  5964  oprabid  6082  f1o2ndf1  6424  poxp  6428  reldmtpos  6484  rntpos  6488  smoiun  6532  tfrlem1  6539  tfrlemi1  6563  tfrexlem  6565  tfri3  6598  nntri3or  6726  qsss  6828  th3qlem1  6871  ixpsnf1o  6971  modom  7061  phplem4  7109  fimax2gtri  7159  fiintim  7191  fisseneq  7195  sbthlemi10  7236  supmoti  7284  suplub2ti  7292  ordiso2  7326  ltmpig  7654  prcdnql  7799  prcunqu  7800  recexprlem1ssl  7948  recexprlem1ssu  7949  recexprlemss1l  7950  recexprlemss1u  7951  cauappcvgprlemladdru  7971  cauappcvgprlemladdrl  7972  caucvgprlemladdrl  7993  mulgt0sr  8093  suplocsrlem  8123  axprecex  8195  ltxrlt  8339  addid0  8646  negf1o  8655  cju  9235  nngt1ne1  9272  nnsub  9276  0mnnnnn0  9528  un0addcl  9529  un0mulcl  9530  zapne  9652  eluzuzle  9862  indstr  9925  elpq  9981  xposdif  10215  ixxdisj  10236  icodisj  10325  uzsubsubfz  10381  elfzmlbp  10466  fzofzim  10527  subfzo0  10588  addmodlteq  10760  seq3f1olemp  10877  seqf1og  10883  expcl2lemap  10913  expnegzap  10935  expaddzap  10945  expmulzap  10947  facwordi  11102  bccl  11129  hashfibclem  11206  hashfibc  11207  hashfacen  11208  fundm2domnop0  11220  wrdind  11414  wrd2ind  11415  swrdccatin1  11417  swrdccatin2  11421  pfxccat3  11426  pfxccat3a  11430  swrdccat3blem  11431  reuccatpfxs1  11439  ovshftex  11504  cau3lem  11799  maxabslemval  11893  rexanre  11905  xrmaxiflemval  11935  2clim  11986  summodc  12069  fsum2dlemstep  12120  fsumiun  12163  prodmodc  12264  fprod2dlemstep  12308  odd2np1lem  12558  oddge22np1  12567  sqoddm1div8z  12572  divalglemeunn  12607  divalglemeuneg  12609  bitsfzo  12641  gcd0id  12675  divgcdcoprm0  12798  prmdvdsexpr  12847  prmfac1  12849  qnumdencl  12884  hashdvds  12918  prm23lt5  12961  pcneg  13023  prmpwdvds  13053  ctinf  13181  imasaddfnlemg  13527  mnd1id  13669  0subm  13697  insubm  13698  dfgrp3mlem  13811  ringrng  14180  domnmuln0  14419  lss1d  14531  islidlm  14627  rnglidlmcl  14628  tgcl  14929  epttop  14955  txbas  15123  txbasval  15132  txcnp  15136  txdis1cn  15143  bldisj  15266  reopnap  15411  dvfgg  15553  lgsdir2lem2  15902  gausslemma2dlem1a  15931  gausslemma2dlem3  15936  gausslemma2d  15942  2lgsoddprmlem2  15979  ushgredgedg  16221  ushgredgedgloop  16223  uhgr0v0e  16229  subumgredg2en  16266  uhgrspansubgrlem  16271  wlk1walkdom  16354  upgriswlkdc  16355  uspgr2wlkeq  16360  clwwlknonex2e  16435  bj-vtoclgft  16547  bj-charfun  16577  bj-charfunbi  16581  bj-indind  16702  bj-nntrans  16721  bj-nnelirr  16723  triap  16813  gfsumval  16862