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  2080  2euex  2125  eqneqall  2370  necon3ad  2402  necon1aidc  2411  necon4addc  2430  elnelall  2467  spcimgft  2828  spcimegft  2830  rspc  2850  rspcimdv  2857  rspc2gv  2868  euind  2939  2reuswapdc  2956  reuind  2957  sbciegft  3008  rspsbc  3060  preqr2g  3785  prel12  3789  intss1  3877  intmin  3882  iinss  3956  disjiun  4016  trel3  4127  trin  4129  repizf2  4183  exmidsssnc  4224  copsexg  4265  po3nr  4331  sowlin  4341  eusvnfb  4475  reusv3  4481  ssorduni  4507  ordsucim  4520  tfis2f  4604  ssrelrel  4747  relop  4798  iss  4974  poirr2  5042  funopg  5272  funssres  5280  funun  5282  funcnvuni  5307  fv3  5560  fvmptt  5631  dff4im  5686  f1eqcocnv  5816  oprabid  5932  f1o2ndf1  6257  poxp  6261  reldmtpos  6282  rntpos  6286  smoiun  6330  tfrlem1  6337  tfrlemi1  6361  tfrexlem  6363  tfri3  6396  nntri3or  6522  qsss  6624  th3qlem1  6667  ixpsnf1o  6766  phplem4  6887  fimax2gtri  6933  fiintim  6961  fisseneq  6964  sbthlemi10  6999  supmoti  7026  suplub2ti  7034  ordiso2  7068  ltmpig  7373  prcdnql  7518  prcunqu  7519  recexprlem1ssl  7667  recexprlem1ssu  7668  recexprlemss1l  7669  recexprlemss1u  7670  cauappcvgprlemladdru  7690  cauappcvgprlemladdrl  7691  caucvgprlemladdrl  7712  mulgt0sr  7812  suplocsrlem  7842  axprecex  7914  ltxrlt  8058  addid0  8365  negf1o  8374  cju  8953  nngt1ne1  8989  nnsub  8993  0mnnnnn0  9243  un0addcl  9244  un0mulcl  9245  zapne  9362  eluzuzle  9571  indstr  9629  elpq  9684  xposdif  9918  ixxdisj  9939  icodisj  10028  uzsubsubfz  10083  elfzmlbp  10168  fzofzim  10224  subfzo0  10278  addmodlteq  10435  seq3f1olemp  10541  expcl2lemap  10572  expnegzap  10594  expaddzap  10604  expmulzap  10606  facwordi  10761  bccl  10788  hashfacen  10857  ovshftex  10869  cau3lem  11164  maxabslemval  11258  rexanre  11270  xrmaxiflemval  11299  2clim  11350  summodc  11432  fsum2dlemstep  11483  fsumiun  11526  prodmodc  11627  fprod2dlemstep  11671  odd2np1lem  11918  oddge22np1  11927  sqoddm1div8z  11932  divalglemeunn  11967  divalglemeuneg  11969  gcd0id  12021  divgcdcoprm0  12144  prmdvdsexpr  12193  prmfac1  12195  qnumdencl  12230  hashdvds  12264  prm23lt5  12306  pcneg  12368  prmpwdvds  12398  ctinf  12492  imasaddfnlemg  12802  mnd1id  12931  0subm  12959  insubm  12960  dfgrp3mlem  13065  ringrng  13415  lss1d  13724  islidlm  13820  rnglidlmcl  13821  tgcl  14049  epttop  14075  txbas  14243  txbasval  14252  txcnp  14256  txdis1cn  14263  bldisj  14386  reopnap  14523  dvfgg  14642  lgsdir2lem2  14916  2lgsoddprmlem2  14940  bj-vtoclgft  15013  bj-charfun  15045  bj-charfunbi  15049  bj-indind  15170  bj-nntrans  15189  bj-nnelirr  15191  triap  15265