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  1942  mor  2125  2euex  2170  eqneqall  2424  necon3ad  2456  necon1aidc  2465  necon4addc  2484  elnelall  2521  spcimgft  2895  spcimegft  2897  rspc  2917  rspcimdv  2924  rspc2gv  2936  euind  3007  2reuswapdc  3024  reuind  3025  sbciegft  3076  rspsbc  3129  preqr2g  3876  prel12  3880  intss1  3969  intmin  3974  iinss  4048  disjiun  4109  trel3  4221  trin  4223  repizf2  4280  exmidsssnc  4321  copsexg  4365  po3nr  4436  sowlin  4446  eusvnfb  4580  reusv3  4586  ssorduni  4614  ordsucim  4627  tfis2f  4711  ssrelrel  4855  relop  4910  iss  5089  poirr2  5160  funopg  5391  funssres  5400  funun  5402  funcnvuni  5430  fv3  5698  fvmptt  5774  dff4im  5828  f1eqcocnv  5970  oprabid  6090  f1o2ndf1  6437  poxp  6441  reldmtpos  6497  rntpos  6501  smoiun  6545  tfrlem1  6552  tfrlemi1  6576  tfrexlem  6578  tfri3  6611  nntri3or  6739  qsss  6841  th3qlem1  6884  ixpsnf1o  6984  modom  7074  phplem4  7122  fimax2gtri  7172  fiintim  7204  fisseneq  7208  sbthlemi10  7249  supmoti  7297  suplub2ti  7305  ordiso2  7339  ltmpig  7670  prcdnql  7815  prcunqu  7816  recexprlem1ssl  7964  recexprlem1ssu  7965  recexprlemss1l  7966  recexprlemss1u  7967  cauappcvgprlemladdru  7987  cauappcvgprlemladdrl  7988  caucvgprlemladdrl  8009  mulgt0sr  8109  suplocsrlem  8139  axprecex  8211  ltxrlt  8355  addid0  8662  negf1o  8672  cju  9252  nngt1ne1  9289  nnsub  9293  0mnnnnn0  9545  un0addcl  9546  un0mulcl  9547  zapne  9669  eluzuzle  9880  indstr  9943  elpq  9999  xposdif  10234  ixxdisj  10255  icodisj  10344  uzsubsubfz  10401  elfzmlbp  10488  fzofzim  10549  subfzo0  10610  addmodlteq  10784  seq3f1olemp  10901  seqf1og  10907  expcl2lemap  10937  expnegzap  10959  expaddzap  10969  expmulzap  10971  facwordi  11127  bccl  11154  hashfibclem  11231  hashfibc  11232  hashfacen  11233  fundm2domnop0  11245  wrdind  11439  wrd2ind  11440  swrdccatin1  11442  swrdccatin2  11446  pfxccat3  11451  pfxccat3a  11455  swrdccat3blem  11456  reuccatpfxs1  11464  ovshftex  11529  cau3lem  11824  maxabslemval  11918  rexanre  11930  xrmaxiflemval  11960  2clim  12011  summodc  12094  fsum2dlemstep  12145  fsumiun  12188  prodmodc  12289  fprod2dlemstep  12333  odd2np1lem  12583  oddge22np1  12592  sqoddm1div8z  12597  divalglemeunn  12632  divalglemeuneg  12634  bitsfzo  12666  gcd0id  12700  divgcdcoprm0  12823  prmdvdsexpr  12872  prmfac1  12874  qnumdencl  12909  hashdvds  12943  prm23lt5  12986  pcneg  13048  prmpwdvds  13078  ctinf  13265  imasaddfnlemg  13578  mnd1id  13711  0subm  13739  insubm  13740  dfgrp3mlem  13853  gfsumval  14102  ringrng  14279  domnmuln0  14520  lss1d  14657  islidlm  14753  rnglidlmcl  14754  tgcl  15055  epttop  15081  txbas  15249  txbasval  15258  txcnp  15262  txdis1cn  15269  bldisj  15392  reopnap  15537  dvfgg  15679  lgsdir2lem2  16028  gausslemma2dlem1a  16057  gausslemma2dlem3  16062  gausslemma2d  16068  2lgsoddprmlem2  16105  ushgredgedg  16347  ushgredgedgloop  16349  uhgr0v0e  16355  subumgredg2en  16392  uhgrspansubgrlem  16397  wlk1walkdom  16480  upgriswlkdc  16481  uspgr2wlkeq  16486  clwwlknonex2e  16561  bj-vtoclgft  16673  bj-charfun  16703  bj-charfunbi  16707  bj-indind  16828  bj-nntrans  16847  bj-nnelirr  16849  triap  16939