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  1643  sbequ2  1783  sbi1v  1906  mor  2087  2euex  2132  eqneqall  2377  necon3ad  2409  necon1aidc  2418  necon4addc  2437  elnelall  2474  spcimgft  2840  spcimegft  2842  rspc  2862  rspcimdv  2869  rspc2gv  2880  euind  2951  2reuswapdc  2968  reuind  2969  sbciegft  3020  rspsbc  3072  preqr2g  3797  prel12  3801  intss1  3889  intmin  3894  iinss  3968  disjiun  4028  trel3  4139  trin  4141  repizf2  4195  exmidsssnc  4236  copsexg  4277  po3nr  4345  sowlin  4355  eusvnfb  4489  reusv3  4495  ssorduni  4523  ordsucim  4536  tfis2f  4620  ssrelrel  4763  relop  4816  iss  4992  poirr2  5062  funopg  5292  funssres  5300  funun  5302  funcnvuni  5327  fv3  5581  fvmptt  5653  dff4im  5708  f1eqcocnv  5838  oprabid  5954  f1o2ndf1  6286  poxp  6290  reldmtpos  6311  rntpos  6315  smoiun  6359  tfrlem1  6366  tfrlemi1  6390  tfrexlem  6392  tfri3  6425  nntri3or  6551  qsss  6653  th3qlem1  6696  ixpsnf1o  6795  phplem4  6916  fimax2gtri  6962  fiintim  6992  fisseneq  6995  sbthlemi10  7032  supmoti  7059  suplub2ti  7067  ordiso2  7101  ltmpig  7406  prcdnql  7551  prcunqu  7552  recexprlem1ssl  7700  recexprlem1ssu  7701  recexprlemss1l  7702  recexprlemss1u  7703  cauappcvgprlemladdru  7723  cauappcvgprlemladdrl  7724  caucvgprlemladdrl  7745  mulgt0sr  7845  suplocsrlem  7875  axprecex  7947  ltxrlt  8092  addid0  8399  negf1o  8408  cju  8988  nngt1ne1  9025  nnsub  9029  0mnnnnn0  9281  un0addcl  9282  un0mulcl  9283  zapne  9400  eluzuzle  9609  indstr  9667  elpq  9723  xposdif  9957  ixxdisj  9978  icodisj  10067  uzsubsubfz  10122  elfzmlbp  10207  fzofzim  10264  subfzo0  10318  addmodlteq  10490  seq3f1olemp  10607  seqf1og  10613  expcl2lemap  10643  expnegzap  10665  expaddzap  10675  expmulzap  10677  facwordi  10832  bccl  10859  hashfacen  10928  ovshftex  10984  cau3lem  11279  maxabslemval  11373  rexanre  11385  xrmaxiflemval  11415  2clim  11466  summodc  11548  fsum2dlemstep  11599  fsumiun  11642  prodmodc  11743  fprod2dlemstep  11787  odd2np1lem  12037  oddge22np1  12046  sqoddm1div8z  12051  divalglemeunn  12086  divalglemeuneg  12088  bitsfzo  12119  gcd0id  12146  divgcdcoprm0  12269  prmdvdsexpr  12318  prmfac1  12320  qnumdencl  12355  hashdvds  12389  prm23lt5  12432  pcneg  12494  prmpwdvds  12524  ctinf  12647  imasaddfnlemg  12957  mnd1id  13088  0subm  13116  insubm  13117  dfgrp3mlem  13230  ringrng  13592  domnmuln0  13829  lss1d  13939  islidlm  14035  rnglidlmcl  14036  tgcl  14300  epttop  14326  txbas  14494  txbasval  14503  txcnp  14507  txdis1cn  14514  bldisj  14637  reopnap  14782  dvfgg  14924  lgsdir2lem2  15270  gausslemma2dlem1a  15299  gausslemma2dlem3  15304  gausslemma2d  15310  2lgsoddprmlem2  15347  bj-vtoclgft  15421  bj-charfun  15453  bj-charfunbi  15457  bj-indind  15578  bj-nntrans  15597  bj-nnelirr  15599  triap  15673