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  1676  ax11i  1760  equveli  1805  eupickbi  2160  nfabdw  2391  rgen2a  2584  reu6  2992  sseq0  3533  disjel  3546  preq12b  3848  prel12  3849  prneimg  3852  elinti  3932  exmidundif  4290  opthreg  4648  elreldm  4950  issref  5111  relcnvtr  5248  relresfld  5258  funopg  5352  funimass2  5399  f0dom0  5519  fvimacnv  5750  funopdmsn  5819  elunirn  5890  oprabid  6033  op1steq  6325  f1o2ndf1  6374  reldmtpos  6399  rntpos  6403  nntri3or  6639  nnaordex  6674  nnawordex  6675  findcard2  7051  findcard2s  7052  mkvprop  7325  cc2lem  7452  lt2addnq  7591  lt2mulnq  7592  genpelvl  7699  genpelvu  7700  distrlem5prl  7773  distrlem5pru  7774  caucvgprlemnkj  7853  map2psrprg  7992  rereceu  8076  ltxrlt  8212  0mnnnnn0  9401  elnnnn0b  9413  nn0le2is012  9529  btwnz  9566  uz11  9745  nn01to3  9812  zq  9821  xrltso  9992  xltnegi  10031  xnn0lenn0nn0  10061  xnn0xadd0  10063  iccleub  10127  fzdcel  10236  uznfz  10299  2ffzeq  10337  elfzonlteqm1  10416  icogelb  10485  flqeqceilz  10540  modqadd1  10583  modqmul1  10599  frecuzrdgtcl  10634  frecuzrdgfunlem  10641  fzfig  10652  seqf1og  10743  m1expeven  10808  qsqeqor  10872  fundm2domnop0  11067  pfxsuff1eqwrdeq  11231  wrdind  11254  wrd2ind  11255  swrdccat3blem  11271  caucvgrelemcau  11491  rexico  11732  fisumss  11903  fsum2dlemstep  11945  ntrivcvgap  12059  fprodssdc  12101  fprod2dlemstep  12133  0dvds  12322  alzdvds  12365  opoe  12406  omoe  12407  opeo  12408  omeo  12409  m1exp1  12412  nn0enne  12413  nn0o1gt2  12416  gcdneg  12503  dfgcd2  12535  algcvgblem  12571  algcvga  12573  eucalglt  12579  coprmdvds  12614  divgcdcoprmex  12624  cncongr1  12625  prm2orodd  12648  prm23lt5  12786  pockthi  12881  f1ocpbl  13344  f1ovscpbl  13345  f1olecpbl  13346  ismnddef  13451  lmodfopnelem1  14288  tg2  14734  tgcl  14738  neii1  14821  neii2  14823  txlm  14953  reopnap  15220  tgioo  15228  addcncntoplem  15235  gausslemma2dlem0i  15736  2lgslem2  15771  2lgs  15783  2lgsoddprmlem3  15790  uhgr0vb  15884  umgredg  15943  uspgrushgr  15978  uspgrupgr  15979  usgruspgr  15981  uhgr2edg  16004  wlkpropg  16037  wlkv  16038  wlkvg  16040  wlkvtxeledgg  16055  wlkl1loop  16069  upgrwlkedg  16072  upgrwlkvtxedg  16075  uspgr2wlkeq  16076  wlkv0  16080  bj-elssuniab  16155  bj-nn0sucALT  16341  triap  16397