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  1679  ax11i  1762  equveli  1807  eupickbi  2162  nfabdw  2394  rgen2a  2587  reu6  2996  sseq0  3538  disjel  3551  preq12b  3858  prel12  3859  prneimg  3862  elinti  3942  exmidundif  4302  opthreg  4660  elreldm  4964  issref  5126  relcnvtr  5263  relresfld  5273  funopg  5367  funimass2  5415  f0dom0  5539  fvimacnv  5771  funopdmsn  5842  elunirn  5917  oprabid  6060  op1steq  6351  f1o2ndf1  6402  fvn0elsuppb  6430  suppfnss  6435  reldmtpos  6462  rntpos  6466  nntri3or  6704  nnaordex  6739  nnawordex  6740  findcard2  7121  findcard2s  7122  mkvprop  7417  cc2lem  7545  lt2addnq  7684  lt2mulnq  7685  genpelvl  7792  genpelvu  7793  distrlem5prl  7866  distrlem5pru  7867  caucvgprlemnkj  7946  map2psrprg  8085  rereceu  8169  ltxrlt  8304  0mnnnnn0  9493  elnnnn0b  9505  nn0le2is012  9623  btwnz  9660  uz11  9840  nn01to3  9912  zq  9921  xrltso  10092  xltnegi  10131  xnn0lenn0nn0  10161  xnn0xadd0  10163  iccleub  10227  fzdcel  10337  uznfz  10400  2ffzeq  10438  elfzonlteqm1  10518  icogelb  10588  flqeqceilz  10643  modqadd1  10686  modqmul1  10702  frecuzrdgtcl  10737  frecuzrdgfunlem  10744  fzfig  10755  seqf1og  10846  m1expeven  10911  qsqeqor  10975  fundm2domnop0  11175  ccatrcl1  11257  pfxsuff1eqwrdeq  11346  wrdind  11369  wrd2ind  11370  swrdccat3blem  11386  caucvgrelemcau  11620  rexico  11861  fisumss  12033  fsum2dlemstep  12075  ntrivcvgap  12189  fprodssdc  12231  fprod2dlemstep  12263  0dvds  12452  alzdvds  12495  opoe  12536  omoe  12537  opeo  12538  omeo  12539  m1exp1  12542  nn0enne  12543  nn0o1gt2  12546  gcdneg  12633  dfgcd2  12665  algcvgblem  12701  algcvga  12703  eucalglt  12709  coprmdvds  12744  divgcdcoprmex  12754  cncongr1  12755  prm2orodd  12778  prm23lt5  12916  pockthi  13011  f1ocpbl  13474  f1ovscpbl  13475  f1olecpbl  13476  ismnddef  13581  lmodfopnelem1  14420  tg2  14871  tgcl  14875  neii1  14958  neii2  14960  txlm  15090  reopnap  15357  tgioo  15365  addcncntoplem  15372  gausslemma2dlem0i  15876  2lgslem2  15911  2lgs  15923  2lgsoddprmlem3  15930  uhgr0vb  16025  umgredg  16086  uspgrushgr  16121  uspgrupgr  16122  usgruspgr  16124  uhgr2edg  16147  edg0usgr  16188  egrsubgr  16204  0uhgrsubgr  16206  uhgrspansubgrlem  16217  vtxdg0v  16235  wlkpropg  16265  wlkv  16267  wlkvg  16269  wlkvtxeledgg  16285  wlkl1loop  16299  upgrwlkedg  16302  upgrwlkvtxedg  16305  uspgr2wlkeq  16306  wlkv0  16310  clwwlkccat  16342  clwwlknp  16358  clwwlkext2edg  16363  eupth2lem3lem4fi  16414  bj-elssuniab  16509  bj-nn0sucALT  16694  triap  16761