Theorem biimtrdi 163

Description: A mixed syllogism inference. (Contributed by NM, 2-Jan-1994.)

Hypotheses

Ref	Expression
biimtrdi.1	|- ( ph -> ( ps <-> ch ) )
biimtrdi.2	|- ( ch -> th )

Assertion

Ref	Expression
biimtrdi	|- ( ph -> ( ps -> th ) )

Proof of Theorem biimtrdi

Step	Hyp	Ref	Expression
1		biimtrdi.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	biimpd 144	. 2 |- ( ph -> ( ps -> ch ) )
3		biimtrdi.2	. 2 |- ( ch -> th )
4	2, 3	syl6 33	1 |- ( ph -> ( ps -> 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:  19.33bdc  1630  ax11i  1714  equveli  1759  eupickbi  2108  nfabdw  2338  rgen2a  2531  reu6  2928  sseq0  3466  disjel  3479  preq12b  3772  prel12  3773  prneimg  3776  elinti  3855  exmidundif  4208  opthreg  4557  elreldm  4855  issref  5013  relcnvtr  5150  relresfld  5160  funopg  5252  funimass2  5296  f0dom0  5411  fvimacnv  5633  elunirn  5769  oprabid  5909  op1steq  6182  f1o2ndf1  6231  reldmtpos  6256  rntpos  6260  nntri3or  6496  nnaordex  6531  nnawordex  6532  findcard2  6891  findcard2s  6892  mkvprop  7158  cc2lem  7267  lt2addnq  7405  lt2mulnq  7406  genpelvl  7513  genpelvu  7514  distrlem5prl  7587  distrlem5pru  7588  caucvgprlemnkj  7667  map2psrprg  7806  rereceu  7890  ltxrlt  8025  0mnnnnn0  9210  elnnnn0b  9222  nn0le2is012  9337  btwnz  9374  uz11  9552  nn01to3  9619  zq  9628  xrltso  9798  xltnegi  9837  xnn0lenn0nn0  9867  xnn0xadd0  9869  iccleub  9933  fzdcel  10042  uznfz  10105  2ffzeq  10143  elfzonlteqm1  10212  icogelb  10268  flqeqceilz  10320  modqadd1  10363  modqmul1  10379  frecuzrdgtcl  10414  frecuzrdgfunlem  10421  fzfig  10432  m1expeven  10569  qsqeqor  10633  caucvgrelemcau  10991  rexico  11232  fisumss  11402  fsum2dlemstep  11444  ntrivcvgap  11558  fprodssdc  11600  fprod2dlemstep  11632  0dvds  11820  alzdvds  11862  opoe  11902  omoe  11903  opeo  11904  omeo  11905  m1exp1  11908  nn0enne  11909  nn0o1gt2  11912  gcdneg  11985  dfgcd2  12017  algcvgblem  12051  algcvga  12053  eucalglt  12059  coprmdvds  12094  divgcdcoprmex  12104  cncongr1  12105  prm2orodd  12128  prm23lt5  12265  pockthi  12358  f1ocpbl  12737  f1ovscpbl  12738  f1olecpbl  12739  ismnddef  12824  lmodfopnelem1  13419  tg2  13645  tgcl  13649  neii1  13732  neii2  13734  txlm  13864  reopnap  14123  tgioo  14131  addcncntoplem  14136  2lgsoddprmlem3  14544  bj-elssuniab  14628  bj-nn0sucALT  14815  triap  14862