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  886  3jao  1312  19.33b2  1640  sbequ2  1780  sbi1v  1903  mor  2084  2euex  2129  eqneqall  2374  necon3ad  2406  necon1aidc  2415  necon4addc  2434  elnelall  2471  spcimgft  2836  spcimegft  2838  rspc  2858  rspcimdv  2865  rspc2gv  2876  euind  2947  2reuswapdc  2964  reuind  2965  sbciegft  3016  rspsbc  3068  preqr2g  3793  prel12  3797  intss1  3885  intmin  3890  iinss  3964  disjiun  4024  trel3  4135  trin  4137  repizf2  4191  exmidsssnc  4232  copsexg  4273  po3nr  4341  sowlin  4351  eusvnfb  4485  reusv3  4491  ssorduni  4519  ordsucim  4532  tfis2f  4616  ssrelrel  4759  relop  4812  iss  4988  poirr2  5058  funopg  5288  funssres  5296  funun  5298  funcnvuni  5323  fv3  5577  fvmptt  5649  dff4im  5704  f1eqcocnv  5834  oprabid  5950  f1o2ndf1  6281  poxp  6285  reldmtpos  6306  rntpos  6310  smoiun  6354  tfrlem1  6361  tfrlemi1  6385  tfrexlem  6387  tfri3  6420  nntri3or  6546  qsss  6648  th3qlem1  6691  ixpsnf1o  6790  phplem4  6911  fimax2gtri  6957  fiintim  6985  fisseneq  6988  sbthlemi10  7025  supmoti  7052  suplub2ti  7060  ordiso2  7094  ltmpig  7399  prcdnql  7544  prcunqu  7545  recexprlem1ssl  7693  recexprlem1ssu  7694  recexprlemss1l  7695  recexprlemss1u  7696  cauappcvgprlemladdru  7716  cauappcvgprlemladdrl  7717  caucvgprlemladdrl  7738  mulgt0sr  7838  suplocsrlem  7868  axprecex  7940  ltxrlt  8085  addid0  8392  negf1o  8401  cju  8980  nngt1ne1  9017  nnsub  9021  0mnnnnn0  9272  un0addcl  9273  un0mulcl  9274  zapne  9391  eluzuzle  9600  indstr  9658  elpq  9714  xposdif  9948  ixxdisj  9969  icodisj  10058  uzsubsubfz  10113  elfzmlbp  10198  fzofzim  10255  subfzo0  10309  addmodlteq  10469  seq3f1olemp  10586  seqf1og  10592  expcl2lemap  10622  expnegzap  10644  expaddzap  10654  expmulzap  10656  facwordi  10811  bccl  10838  hashfacen  10907  ovshftex  10963  cau3lem  11258  maxabslemval  11352  rexanre  11364  xrmaxiflemval  11393  2clim  11444  summodc  11526  fsum2dlemstep  11577  fsumiun  11620  prodmodc  11721  fprod2dlemstep  11765  odd2np1lem  12013  oddge22np1  12022  sqoddm1div8z  12027  divalglemeunn  12062  divalglemeuneg  12064  gcd0id  12116  divgcdcoprm0  12239  prmdvdsexpr  12288  prmfac1  12290  qnumdencl  12325  hashdvds  12359  prm23lt5  12401  pcneg  12463  prmpwdvds  12493  ctinf  12587  imasaddfnlemg  12897  mnd1id  13028  0subm  13056  insubm  13057  dfgrp3mlem  13170  ringrng  13532  domnmuln0  13769  lss1d  13879  islidlm  13975  rnglidlmcl  13976  tgcl  14232  epttop  14258  txbas  14426  txbasval  14435  txcnp  14439  txdis1cn  14446  bldisj  14569  reopnap  14706  dvfgg  14842  lgsdir2lem2  15145  gausslemma2dlem1a  15174  gausslemma2dlem3  15179  gausslemma2d  15185  2lgsoddprmlem2  15194  bj-vtoclgft  15267  bj-charfun  15299  bj-charfunbi  15303  bj-indind  15424  bj-nntrans  15443  bj-nnelirr  15445  triap  15519