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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117

This theorem is used by:  19.33bdc  1683  ax11i  1766  equveli  1812  eupickbi  2169  nfabdw  2411  rgen2a  2604  reu6  3015  disjel  3579  preq12b  3895  prel12  3896  prneimg  3899  elinti  3979  exmidundif  4343  opthreg  4703  elreldm  5008  issref  5170  relcnvtr  5307  relresfld  5317  funopg  5411  funimass2  5459  f0dom0  5586  fvimacnv  5824  funopdmsn  5895  elunirn  5972  oprabid  6117  op1steq  6413  f1o2ndf1  6464  fvn0elsuppb  6492  suppfnss  6497  reldmtpos  6524  rntpos  6528  nntri3or  6766  nnaordex  6801  nnawordex  6802  findcard2  7193  findcard2s  7194  mkvprop  7498  cc2lem  7632  lt2addnq  7771  lt2mulnq  7772  genpelvl  7879  genpelvu  7880  distrlem5prl  7953  distrlem5pru  7954  caucvgprlemnkj  8033  map2psrprg  8172  rereceu  8256  ltxrlt  8391  0mnnnnn0  9599  elnnnn0b  9611  nn0le2is012  9732  btwnz  9769  uz11  9954  nn01to3  10026  zq  10035  xrltso  10208  xltnegi  10247  xnn0lenn0nn0  10277  xnn0xadd0  10279  iccleub  10343  fzdcel  10454  uznfz  10520  2ffzeq  10558  elfzonlteqm1  10638  icogelb  10710  flqeqceilz  10768  modqadd1  10811  modqmul1  10827  frecuzrdgtcl  10862  frecuzrdgfunlem  10869  fzfig  10880  seqf1og  10971  m1expeven  11036  qsqeqor  11100  hashf1lem2  11300  fundm2domnop0  11314  ccatrcl1  11396  pfxsuff1eqwrdeq  11485  wrdind  11508  wrd2ind  11509  swrdccat3blem  11525  caucvgrelemcau  11760  rexico  12002  fisumss  12175  fsum2dlemstep  12217  ntrivcvgap  12331  fprodssdc  12373  fprod2dlemstep  12405  0dvds  12594  alzdvds  12637  opoe  12678  omoe  12679  opeo  12680  omeo  12681  m1exp1  12684  nn0enne  12685  nn0o1gt2  12688  gcdneg  12775  dfgcd2  12807  algcvgblem  12843  algcvga  12845  eucalglt  12851  coprmdvds  12886  divgcdcoprmex  12896  cncongr1  12897  prm2orodd  12920  prm23lt5  13062  pockthi  13157  ballotfilemfc0  13281  ballotfilemfcc  13282  f1ocpbl  13681  f1ovscpbl  13682  f1olecpbl  13683  ismnddef  13780  lmodfopnelem1  14710  tg2  15210  tgcl  15214  neii1  15297  neii2  15299  txlm  15429  reopnap  15696  tgioo  15704  addcncntoplem  15711  birthdaylem1g  16144  gausslemma2dlem0i  16274  2lgslem2  16309  2lgs  16321  2lgsoddprmlem3  16328  uhgr0vb  16423  umgredg  16484  uspgrushgr  16519  uspgrupgr  16520  usgruspgr  16522  uhgr2edg  16545  edg0usgr  16586  egrsubgr  16602  0uhgrsubgr  16604  uhgrspansubgrlem  16615  vtxdg0v  16633  wlkpropg  16663  wlkv  16665  wlkvg  16667  wlkvtxeledgg  16683  wlkl1loop  16697  upgrwlkedg  16700  upgrwlkvtxedg  16703  uspgr2wlkeq  16704  wlkv0  16708  clwwlkccat  16740  clwwlknp  16756  clwwlkext2edg  16761  eupth2lem3lem4fi  16812  bj-elssuniab  16917  bj-nn0sucALT  17102  triap  17176