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  887  3jao  1314  19.33b2  1652  sbequ2  1792  sbi1v  1915  mor  2096  2euex  2141  eqneqall  2386  necon3ad  2418  necon1aidc  2427  necon4addc  2446  elnelall  2483  spcimgft  2849  spcimegft  2851  rspc  2871  rspcimdv  2878  rspc2gv  2889  euind  2960  2reuswapdc  2977  reuind  2978  sbciegft  3029  rspsbc  3081  preqr2g  3808  prel12  3812  intss1  3900  intmin  3905  iinss  3979  disjiun  4039  trel3  4150  trin  4152  repizf2  4206  exmidsssnc  4247  copsexg  4288  po3nr  4357  sowlin  4367  eusvnfb  4501  reusv3  4507  ssorduni  4535  ordsucim  4548  tfis2f  4632  ssrelrel  4775  relop  4828  iss  5005  poirr2  5075  funopg  5305  funssres  5313  funun  5315  funcnvuni  5343  fv3  5599  fvmptt  5671  dff4im  5726  f1eqcocnv  5860  oprabid  5976  f1o2ndf1  6314  poxp  6318  reldmtpos  6339  rntpos  6343  smoiun  6387  tfrlem1  6394  tfrlemi1  6418  tfrexlem  6420  tfri3  6453  nntri3or  6579  qsss  6681  th3qlem1  6724  ixpsnf1o  6823  phplem4  6952  fimax2gtri  6998  fiintim  7028  fisseneq  7031  sbthlemi10  7068  supmoti  7095  suplub2ti  7103  ordiso2  7137  ltmpig  7452  prcdnql  7597  prcunqu  7598  recexprlem1ssl  7746  recexprlem1ssu  7747  recexprlemss1l  7748  recexprlemss1u  7749  cauappcvgprlemladdru  7769  cauappcvgprlemladdrl  7770  caucvgprlemladdrl  7791  mulgt0sr  7891  suplocsrlem  7921  axprecex  7993  ltxrlt  8138  addid0  8445  negf1o  8454  cju  9034  nngt1ne1  9071  nnsub  9075  0mnnnnn0  9327  un0addcl  9328  un0mulcl  9329  zapne  9447  eluzuzle  9656  indstr  9714  elpq  9770  xposdif  10004  ixxdisj  10025  icodisj  10114  uzsubsubfz  10169  elfzmlbp  10254  fzofzim  10312  subfzo0  10371  addmodlteq  10543  seq3f1olemp  10660  seqf1og  10666  expcl2lemap  10696  expnegzap  10718  expaddzap  10728  expmulzap  10730  facwordi  10885  bccl  10912  hashfacen  10981  fundm2domnop0  10990  ovshftex  11130  cau3lem  11425  maxabslemval  11519  rexanre  11531  xrmaxiflemval  11561  2clim  11612  summodc  11694  fsum2dlemstep  11745  fsumiun  11788  prodmodc  11889  fprod2dlemstep  11933  odd2np1lem  12183  oddge22np1  12192  sqoddm1div8z  12197  divalglemeunn  12232  divalglemeuneg  12234  bitsfzo  12266  gcd0id  12300  divgcdcoprm0  12423  prmdvdsexpr  12472  prmfac1  12474  qnumdencl  12509  hashdvds  12543  prm23lt5  12586  pcneg  12648  prmpwdvds  12678  ctinf  12801  imasaddfnlemg  13146  mnd1id  13288  0subm  13316  insubm  13317  dfgrp3mlem  13430  ringrng  13798  domnmuln0  14035  lss1d  14145  islidlm  14241  rnglidlmcl  14242  tgcl  14536  epttop  14562  txbas  14730  txbasval  14739  txcnp  14743  txdis1cn  14750  bldisj  14873  reopnap  15018  dvfgg  15160  lgsdir2lem2  15506  gausslemma2dlem1a  15535  gausslemma2dlem3  15540  gausslemma2d  15546  2lgsoddprmlem2  15583  bj-vtoclgft  15711  bj-charfun  15743  bj-charfunbi  15747  bj-indind  15868  bj-nntrans  15887  bj-nnelirr  15889  triap  15968