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  4345  opthreg  4705  elreldm  5010  issref  5173  relcnvtr  5310  relresfld  5320  funopg  5414  funimass2  5462  f0dom0  5589  fvimacnv  5827  funopdmsn  5898  elunirn  5975  oprabid  6120  op1steq  6417  f1o2ndf1  6468  fvn0elsuppb  6496  suppfnss  6501  reldmtpos  6528  rntpos  6532  nntri3or  6770  nnaordex  6805  nnawordex  6806  findcard2  7197  findcard2s  7198  mkvprop  7504  cc2lem  7638  lt2addnq  7777  lt2mulnq  7778  genpelvl  7885  genpelvu  7886  distrlem5prl  7959  distrlem5pru  7960  caucvgprlemnkj  8039  map2psrprg  8178  rereceu  8262  ltxrlt  8397  0mnnnnn0  9606  elnnnn0b  9618  nn0le2is012  9739  btwnz  9776  uz11  9961  nn01to3  10033  zq  10042  xrltso  10215  xltnegi  10254  xnn0lenn0nn0  10284  xnn0xadd0  10286  iccleub  10350  fzdcel  10461  uznfz  10527  2ffzeq  10565  elfzonlteqm1  10645  icogelb  10717  flqeqceilz  10776  modqadd1  10819  modqmul1  10835  frecuzrdgtcl  10870  frecuzrdgfunlem  10877  fzfig  10888  seqf1og  10979  m1expeven  11044  qsqeqor  11108  hashf1lem2  11308  fundm2domnop0  11322  ccatrcl1  11404  pfxsuff1eqwrdeq  11493  wrdind  11516  wrd2ind  11517  swrdccat3blem  11533  caucvgrelemcau  11768  rexico  12010  fisumss  12184  fsum2dlemstep  12226  ntrivcvgap  12340  fprodssdc  12382  fprod2dlemstep  12414  0dvds  12603  alzdvds  12646  opoe  12687  omoe  12688  opeo  12689  omeo  12690  m1exp1  12693  nn0enne  12694  nn0o1gt2  12697  gcdneg  12784  dfgcd2  12816  algcvgblem  12852  algcvga  12854  eucalglt  12860  coprmdvds  12895  divgcdcoprmex  12905  cncongr1  12906  prm2orodd  12929  prm23lt5  13071  pockthi  13166  ballotfilemfc0  13290  ballotfilemfcc  13291  f1ocpbl  13691  f1ovscpbl  13692  f1olecpbl  13693  ismnddef  13790  lmodfopnelem1  14770  tg2  15283  tgcl  15287  neii1  15370  neii2  15372  txlm  15502  reopnap  15769  tgioo  15777  addcncntoplem  15784  sineq0re  16073  birthdaylem1g  16222  gausslemma2dlem0i  16378  2lgslem2  16413  2lgs  16425  2lgsoddprmlem3  16432  uhgr0vb  16527  umgredg  16588  uspgrushgr  16623  uspgrupgr  16624  usgruspgr  16626  uhgr2edg  16649  edg0usgr  16690  egrsubgr  16706  0uhgrsubgr  16708  uhgrspansubgrlem  16719  vtxdg0v  16737  wlkpropg  16767  wlkv  16769  wlkvg  16771  wlkvtxeledgg  16787  wlkl1loop  16801  upgrwlkedg  16804  upgrwlkvtxedg  16807  uspgr2wlkeq  16808  wlkv0  16812  clwwlkccat  16844  clwwlknp  16860  clwwlkext2edg  16865  eupth2lem3lem4fi  16916  bj-elssuniab  17021  bj-nn0sucALT  17206  triap  17281