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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117

This theorem is used by:  3imtr4g  205  ancomsd  269  pm2.13dc  897  3jao  1342  19.33b2  1682  sbequ2  1822  sbi1v  1946  mor  2129  2euex  2174  eqneqall  2430  necon3ad  2462  necon1aidc  2471  necon4addc  2490  elnelall  2527  spcimgft  2901  spcimegft  2903  rspc  2923  rspcimdv  2930  rspc2gv  2942  euind  3013  2reuswapdc  3030  reuind  3031  sbciegft  3082  rspsbc  3135  preqr2g  3892  prel12  3896  intss1  3985  intmin  3990  iinss  4064  disjiun  4125  trel3  4239  trin  4241  repizf2  4301  exmidsssnc  4342  copsexg  4386  po3nr  4457  sowlin  4467  eusvnfb  4602  reusv3  4608  ssorduni  4636  ordsucim  4649  tfis2f  4733  ssrelrel  4877  relop  4932  iss  5112  poirr2  5183  funopg  5414  funssres  5423  funun  5425  funcnvuni  5453  fv3  5721  fvmptt  5800  dff4im  5857  f1eqcocnv  6000  oprabid  6120  f1o2ndf1  6468  poxp  6472  reldmtpos  6529  rntpos  6533  smoiun  6577  tfrlem1  6584  tfrlemi1  6608  tfrexlem  6610  tfri3  6643  nntri3or  6771  qsss  6873  th3qlem1  6916  ixpsnf1o  7024  modom  7114  phplem4  7162  fimax2gtri  7212  fiintim  7244  fisseneq  7248  sbthlemi10  7290  supmoti  7339  suplub2ti  7347  ordiso2  7381  ltmpig  7712  prcdnql  7857  prcunqu  7858  recexprlem1ssl  8006  recexprlem1ssu  8007  recexprlemss1l  8008  recexprlemss1u  8009  cauappcvgprlemladdru  8029  cauappcvgprlemladdrl  8030  caucvgprlemladdrl  8051  mulgt0sr  8151  suplocsrlem  8181  axprecex  8253  ltxrlt  8397  addid0  8706  negf1o  8716  cju  9299  nngt1ne1  9348  nnsub  9352  0mnnnnn0  9606  un0addcl  9607  un0mulcl  9608  zapne  9728  eluzuzle  9945  indstr  10008  elpq  10065  xposdif  10300  ixxdisj  10321  icodisj  10410  uzsubsubfz  10468  elfzmlbp  10555  fzofzim  10616  subfzo0  10677  addmodlteq  10855  seq3f1olemp  10972  seqf1og  10978  expcl2lemap  11008  expnegzap  11030  expaddzap  11040  expmulzap  11042  facwordi  11199  bccl  11226  hashfibclem  11303  hashfibc  11304  hashfacen  11305  hashf1lem1  11306  hashf1  11308  fundm2domnop0  11321  wrdind  11515  wrd2ind  11516  swrdccatin1  11518  swrdccatin2  11522  pfxccat3  11527  pfxccat3a  11531  swrdccat3blem  11532  reuccatpfxs1  11540  ovshftex  11605  cau3lem  11902  maxabslemval  11996  rexanre  12008  xrmaxiflemval  12040  2clim  12091  summodc  12174  fsum2dlemstep  12225  fsumiun  12268  prodmodc  12369  fprod2dlemstep  12413  odd2np1lem  12663  oddge22np1  12672  sqoddm1div8z  12677  divalglemeunn  12712  divalglemeuneg  12714  bitsfzo  12746  gcd0id  12780  divgcdcoprm0  12903  prmdvdsexpr  12953  prmfac1  12955  qnumdencl  12991  nn0sqdcq  13012  hashdvds  13027  prm23lt5  13070  pcneg  13132  prmpwdvds  13162  prmlem0  13248  ctinf  13378  imasaddfnlemg  13693  mnd1id  13821  0subm  13849  insubm  13850  dfgrp3mlem  13961  gsumvalfi  14241  gsum2d2fi  14273  ringrng  14447  domnmuln0  14690  lss1d  14828  islidlm  14924  rnglidlmcl  14925  gsumfsum  15031  psrbagmaxlem1  15178  mvrf1fi  15219  tgcl  15307  epttop  15333  txbas  15501  txbasval  15510  txcnp  15514  txdis1cn  15521  bldisj  15644  reopnap  15789  dvfgg  15931  rpcxpmul2z  16165  ppiublem1  16308  lgsdir2lem2  16370  gausslemma2dlem1a  16399  gausslemma2dlem3  16404  gausslemma2d  16410  2lgsoddprmlem2  16447  ushgredgedg  16689  ushgredgedgloop  16691  uhgr0v0e  16697  subumgredg2en  16734  uhgrspansubgrlem  16739  wlk1walkdom  16822  upgriswlkdc  16823  uspgr2wlkeq  16828  clwwlknonex2e  16903  bj-vtoclgft  17025  bj-charfun  17055  bj-charfunbi  17059  bj-indind  17180  bj-nntrans  17199  bj-nnelirr  17201  triap  17301