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  6529  rntpos  6533  nntri3or  6771  nnaordex  6806  nnawordex  6807  findcard2  7199  findcard2s  7200  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  9737  btwnz  9775  uz11  9960  nn01to3  10032  zq  10041  xrltso  10214  xltnegi  10253  xnn0lenn0nn0  10283  xnn0xadd0  10285  iccleub  10349  fzdcel  10460  uznfz  10526  2ffzeq  10564  elfzonlteqm1  10644  icogelb  10716  flqeqceilz  10775  modqadd1  10818  modqmul1  10834  frecuzrdgtcl  10869  frecuzrdgfunlem  10876  fzfig  10887  seqf1og  10978  m1expeven  11043  qsqeqor  11107  hashf1lem2  11307  fundm2domnop0  11321  ccatrcl1  11403  pfxsuff1eqwrdeq  11492  wrdind  11515  wrd2ind  11516  swrdccat3blem  11532  caucvgrelemcau  11767  rexico  12009  fisumss  12183  fsum2dlemstep  12225  ntrivcvgap  12339  fprodssdc  12381  fprod2dlemstep  12413  0dvds  12602  alzdvds  12645  opoe  12686  omoe  12687  opeo  12688  omeo  12689  m1exp1  12692  nn0enne  12693  nn0o1gt2  12696  gcdneg  12783  dfgcd2  12815  algcvgblem  12851  algcvga  12853  eucalglt  12859  coprmdvds  12894  divgcdcoprmex  12904  cncongr1  12905  prm2orodd  12928  prm23lt5  13070  pockthi  13165  ballotfilemfc0  13289  ballotfilemfcc  13290  f1ocpbl  13690  f1ovscpbl  13691  f1olecpbl  13692  ismnddef  13789  lmodfopnelem1  14769  tg2  15303  tgcl  15307  neii1  15390  neii2  15392  txlm  15522  reopnap  15789  tgioo  15797  addcncntoplem  15804  sineq0re  16093  birthdaylem1g  16242  gausslemma2dlem0i  16398  2lgslem2  16433  2lgs  16445  2lgsoddprmlem3  16452  uhgr0vb  16547  umgredg  16608  uspgrushgr  16643  uspgrupgr  16644  usgruspgr  16646  uhgr2edg  16669  edg0usgr  16710  egrsubgr  16726  0uhgrsubgr  16728  uhgrspansubgrlem  16739  vtxdg0v  16757  wlkpropg  16787  wlkv  16789  wlkvg  16791  wlkvtxeledgg  16807  wlkl1loop  16821  upgrwlkedg  16824  upgrwlkvtxedg  16827  uspgr2wlkeq  16828  wlkv0  16832  clwwlkccat  16864  clwwlknp  16880  clwwlkext2edg  16885  eupth2lem3lem4fi  16936  bj-elssuniab  17041  bj-nn0sucALT  17226  triap  17301