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  885  3jao  1301  19.33b2  1629  sbequ2  1769  sbi1v  1891  mor  2068  2euex  2113  eqneqall  2357  necon3ad  2389  necon1aidc  2398  necon4addc  2417  elnelall  2454  spcimgft  2815  spcimegft  2817  rspc  2837  rspcimdv  2844  rspc2gv  2855  euind  2926  2reuswapdc  2943  reuind  2944  sbciegft  2995  rspsbc  3047  preqr2g  3769  prel12  3773  intss1  3861  intmin  3866  iinss  3940  disjiun  4000  trel3  4111  trin  4113  repizf2  4164  exmidsssnc  4205  copsexg  4246  po3nr  4312  sowlin  4322  eusvnfb  4456  reusv3  4462  ssorduni  4488  ordsucim  4501  tfis2f  4585  ssrelrel  4728  relop  4779  iss  4955  poirr2  5023  funopg  5252  funssres  5260  funun  5262  funcnvuni  5287  fv3  5540  fvmptt  5609  dff4im  5664  f1eqcocnv  5794  oprabid  5909  f1o2ndf1  6231  poxp  6235  reldmtpos  6256  rntpos  6260  smoiun  6304  tfrlem1  6311  tfrlemi1  6335  tfrexlem  6337  tfri3  6370  nntri3or  6496  qsss  6596  th3qlem1  6639  ixpsnf1o  6738  phplem4  6857  fimax2gtri  6903  fiintim  6930  fisseneq  6933  sbthlemi10  6967  supmoti  6994  suplub2ti  7002  ordiso2  7036  ltmpig  7340  prcdnql  7485  prcunqu  7486  recexprlem1ssl  7634  recexprlem1ssu  7635  recexprlemss1l  7636  recexprlemss1u  7637  cauappcvgprlemladdru  7657  cauappcvgprlemladdrl  7658  caucvgprlemladdrl  7679  mulgt0sr  7779  suplocsrlem  7809  axprecex  7881  ltxrlt  8025  addid0  8332  negf1o  8341  cju  8920  nngt1ne1  8956  nnsub  8960  0mnnnnn0  9210  un0addcl  9211  un0mulcl  9212  zapne  9329  eluzuzle  9538  indstr  9595  elpq  9650  xposdif  9884  ixxdisj  9905  icodisj  9994  uzsubsubfz  10049  elfzmlbp  10134  fzofzim  10190  subfzo0  10244  addmodlteq  10400  seq3f1olemp  10504  expcl2lemap  10534  expnegzap  10556  expaddzap  10566  expmulzap  10568  facwordi  10722  bccl  10749  hashfacen  10818  ovshftex  10830  cau3lem  11125  maxabslemval  11219  rexanre  11231  xrmaxiflemval  11260  2clim  11311  summodc  11393  fsum2dlemstep  11444  fsumiun  11487  prodmodc  11588  fprod2dlemstep  11632  odd2np1lem  11879  oddge22np1  11888  sqoddm1div8z  11893  divalglemeunn  11928  divalglemeuneg  11930  gcd0id  11982  divgcdcoprm0  12103  prmdvdsexpr  12152  prmfac1  12154  qnumdencl  12189  hashdvds  12223  prm23lt5  12265  pcneg  12326  prmpwdvds  12355  ctinf  12433  imasaddfnlemg  12740  mnd1id  12853  0subm  12876  insubm  12877  dfgrp3mlem  12973  lss1d  13475  tgcl  13649  epttop  13675  txbas  13843  txbasval  13852  txcnp  13856  txdis1cn  13863  bldisj  13986  reopnap  14123  dvfgg  14242  lgsdir2lem2  14515  2lgsoddprmlem2  14539  bj-vtoclgft  14612  bj-charfun  14644  bj-charfunbi  14648  bj-indind  14769  bj-nntrans  14788  bj-nnelirr  14790  triap  14862