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  1644  ax11i  1728  equveli  1773  eupickbi  2127  nfabdw  2358  rgen2a  2551  reu6  2953  sseq0  3492  disjel  3505  preq12b  3800  prel12  3801  prneimg  3804  elinti  3883  exmidundif  4239  opthreg  4592  elreldm  4892  issref  5052  relcnvtr  5189  relresfld  5199  funopg  5292  funimass2  5336  f0dom0  5451  fvimacnv  5677  elunirn  5813  oprabid  5954  op1steq  6237  f1o2ndf1  6286  reldmtpos  6311  rntpos  6315  nntri3or  6551  nnaordex  6586  nnawordex  6587  findcard2  6950  findcard2s  6951  mkvprop  7224  cc2lem  7333  lt2addnq  7471  lt2mulnq  7472  genpelvl  7579  genpelvu  7580  distrlem5prl  7653  distrlem5pru  7654  caucvgprlemnkj  7733  map2psrprg  7872  rereceu  7956  ltxrlt  8092  0mnnnnn0  9281  elnnnn0b  9293  nn0le2is012  9408  btwnz  9445  uz11  9624  nn01to3  9691  zq  9700  xrltso  9871  xltnegi  9910  xnn0lenn0nn0  9940  xnn0xadd0  9942  iccleub  10006  fzdcel  10115  uznfz  10178  2ffzeq  10216  elfzonlteqm1  10286  icogelb  10355  flqeqceilz  10410  modqadd1  10453  modqmul1  10469  frecuzrdgtcl  10504  frecuzrdgfunlem  10511  fzfig  10522  seqf1og  10613  m1expeven  10678  qsqeqor  10742  caucvgrelemcau  11145  rexico  11386  fisumss  11557  fsum2dlemstep  11599  ntrivcvgap  11713  fprodssdc  11755  fprod2dlemstep  11787  0dvds  11976  alzdvds  12019  opoe  12060  omoe  12061  opeo  12062  omeo  12063  m1exp1  12066  nn0enne  12067  nn0o1gt2  12070  gcdneg  12149  dfgcd2  12181  algcvgblem  12217  algcvga  12219  eucalglt  12225  coprmdvds  12260  divgcdcoprmex  12270  cncongr1  12271  prm2orodd  12294  prm23lt5  12432  pockthi  12527  f1ocpbl  12954  f1ovscpbl  12955  f1olecpbl  12956  ismnddef  13059  lmodfopnelem1  13880  tg2  14296  tgcl  14300  neii1  14383  neii2  14385  txlm  14515  reopnap  14782  tgioo  14790  addcncntoplem  14797  gausslemma2dlem0i  15298  2lgslem2  15333  2lgs  15345  2lgsoddprmlem3  15352  bj-elssuniab  15437  bj-nn0sucALT  15624  triap  15673