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  1640  ax11i  1724  equveli  1769  eupickbi  2119  nfabdw  2350  rgen2a  2543  reu6  2940  sseq0  3478  disjel  3491  preq12b  3784  prel12  3785  prneimg  3788  elinti  3867  exmidundif  4220  opthreg  4569  elreldm  4867  issref  5025  relcnvtr  5162  relresfld  5172  funopg  5264  funimass2  5308  f0dom0  5423  fvimacnv  5646  elunirn  5782  oprabid  5922  op1steq  6197  f1o2ndf1  6246  reldmtpos  6271  rntpos  6275  nntri3or  6511  nnaordex  6546  nnawordex  6547  findcard2  6906  findcard2s  6907  mkvprop  7173  cc2lem  7282  lt2addnq  7420  lt2mulnq  7421  genpelvl  7528  genpelvu  7529  distrlem5prl  7602  distrlem5pru  7603  caucvgprlemnkj  7682  map2psrprg  7821  rereceu  7905  ltxrlt  8040  0mnnnnn0  9225  elnnnn0b  9237  nn0le2is012  9352  btwnz  9389  uz11  9567  nn01to3  9634  zq  9643  xrltso  9813  xltnegi  9852  xnn0lenn0nn0  9882  xnn0xadd0  9884  iccleub  9948  fzdcel  10057  uznfz  10120  2ffzeq  10158  elfzonlteqm1  10227  icogelb  10283  flqeqceilz  10335  modqadd1  10378  modqmul1  10394  frecuzrdgtcl  10429  frecuzrdgfunlem  10436  fzfig  10447  m1expeven  10584  qsqeqor  10648  caucvgrelemcau  11006  rexico  11247  fisumss  11417  fsum2dlemstep  11459  ntrivcvgap  11573  fprodssdc  11615  fprod2dlemstep  11647  0dvds  11835  alzdvds  11877  opoe  11917  omoe  11918  opeo  11919  omeo  11920  m1exp1  11923  nn0enne  11924  nn0o1gt2  11927  gcdneg  12000  dfgcd2  12032  algcvgblem  12066  algcvga  12068  eucalglt  12074  coprmdvds  12109  divgcdcoprmex  12119  cncongr1  12120  prm2orodd  12143  prm23lt5  12280  pockthi  12373  f1ocpbl  12753  f1ovscpbl  12754  f1olecpbl  12755  ismnddef  12844  lmodfopnelem1  13600  tg2  13943  tgcl  13947  neii1  14030  neii2  14032  txlm  14162  reopnap  14421  tgioo  14429  addcncntoplem  14434  2lgsoddprmlem3  14842  bj-elssuniab  14926  bj-nn0sucALT  15113  triap  15161