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  1653  sbequ2  1793  sbi1v  1916  mor  2098  2euex  2143  eqneqall  2388  necon3ad  2420  necon1aidc  2429  necon4addc  2448  elnelall  2485  spcimgft  2856  spcimegft  2858  rspc  2878  rspcimdv  2885  rspc2gv  2896  euind  2967  2reuswapdc  2984  reuind  2985  sbciegft  3036  rspsbc  3089  preqr2g  3821  prel12  3825  intss1  3914  intmin  3919  iinss  3993  disjiun  4054  trel3  4166  trin  4168  repizf2  4222  exmidsssnc  4263  copsexg  4306  po3nr  4375  sowlin  4385  eusvnfb  4519  reusv3  4525  ssorduni  4553  ordsucim  4566  tfis2f  4650  ssrelrel  4793  relop  4846  iss  5024  poirr2  5094  funopg  5324  funssres  5332  funun  5334  funcnvuni  5362  fv3  5622  fvmptt  5694  dff4im  5749  f1eqcocnv  5883  oprabid  5999  f1o2ndf1  6337  poxp  6341  reldmtpos  6362  rntpos  6366  smoiun  6410  tfrlem1  6417  tfrlemi1  6441  tfrexlem  6443  tfri3  6476  nntri3or  6602  qsss  6704  th3qlem1  6747  ixpsnf1o  6846  phplem4  6977  fimax2gtri  7024  fiintim  7054  fisseneq  7057  sbthlemi10  7094  supmoti  7121  suplub2ti  7129  ordiso2  7163  ltmpig  7487  prcdnql  7632  prcunqu  7633  recexprlem1ssl  7781  recexprlem1ssu  7782  recexprlemss1l  7783  recexprlemss1u  7784  cauappcvgprlemladdru  7804  cauappcvgprlemladdrl  7805  caucvgprlemladdrl  7826  mulgt0sr  7926  suplocsrlem  7956  axprecex  8028  ltxrlt  8173  addid0  8480  negf1o  8489  cju  9069  nngt1ne1  9106  nnsub  9110  0mnnnnn0  9362  un0addcl  9363  un0mulcl  9364  zapne  9482  eluzuzle  9691  indstr  9749  elpq  9805  xposdif  10039  ixxdisj  10060  icodisj  10149  uzsubsubfz  10204  elfzmlbp  10289  fzofzim  10349  subfzo0  10408  addmodlteq  10580  seq3f1olemp  10697  seqf1og  10703  expcl2lemap  10733  expnegzap  10755  expaddzap  10765  expmulzap  10767  facwordi  10922  bccl  10949  hashfacen  11018  fundm2domnop0  11027  wrdind  11213  wrd2ind  11214  swrdccatin1  11216  swrdccatin2  11220  pfxccat3  11225  pfxccat3a  11229  swrdccat3blem  11230  reuccatpfxs1  11238  ovshftex  11245  cau3lem  11540  maxabslemval  11634  rexanre  11646  xrmaxiflemval  11676  2clim  11727  summodc  11809  fsum2dlemstep  11860  fsumiun  11903  prodmodc  12004  fprod2dlemstep  12048  odd2np1lem  12298  oddge22np1  12307  sqoddm1div8z  12312  divalglemeunn  12347  divalglemeuneg  12349  bitsfzo  12381  gcd0id  12415  divgcdcoprm0  12538  prmdvdsexpr  12587  prmfac1  12589  qnumdencl  12624  hashdvds  12658  prm23lt5  12701  pcneg  12763  prmpwdvds  12793  ctinf  12916  imasaddfnlemg  13261  mnd1id  13403  0subm  13431  insubm  13432  dfgrp3mlem  13545  ringrng  13913  domnmuln0  14150  lss1d  14260  islidlm  14356  rnglidlmcl  14357  tgcl  14651  epttop  14677  txbas  14845  txbasval  14854  txcnp  14858  txdis1cn  14865  bldisj  14988  reopnap  15133  dvfgg  15275  lgsdir2lem2  15621  gausslemma2dlem1a  15650  gausslemma2dlem3  15655  gausslemma2d  15661  2lgsoddprmlem2  15698  bj-vtoclgft  15911  bj-charfun  15942  bj-charfunbi  15946  bj-indind  16067  bj-nntrans  16086  bj-nnelirr  16088  triap  16170