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  1808  eupickbi  2163  nfabdw  2403  rgen2a  2596  reu6  3006  sseq0  3550  disjel  3563  preq12b  3874  prel12  3875  prneimg  3878  elinti  3958  exmidundif  4319  opthreg  4678  elreldm  4983  issref  5145  relcnvtr  5282  relresfld  5292  funopg  5386  funimass2  5434  f0dom0  5561  fvimacnv  5793  funopdmsn  5864  elunirn  5939  oprabid  6082  op1steq  6373  f1o2ndf1  6424  fvn0elsuppb  6452  suppfnss  6457  reldmtpos  6484  rntpos  6488  nntri3or  6726  nnaordex  6761  nnawordex  6762  findcard2  7146  findcard2s  7147  mkvprop  7449  cc2lem  7580  lt2addnq  7719  lt2mulnq  7720  genpelvl  7827  genpelvu  7828  distrlem5prl  7901  distrlem5pru  7902  caucvgprlemnkj  7981  map2psrprg  8120  rereceu  8204  ltxrlt  8339  0mnnnnn0  9528  elnnnn0b  9540  nn0le2is012  9660  btwnz  9697  uz11  9877  nn01to3  9949  zq  9958  xrltso  10129  xltnegi  10168  xnn0lenn0nn0  10198  xnn0xadd0  10200  iccleub  10264  fzdcel  10374  uznfz  10437  2ffzeq  10475  elfzonlteqm1  10555  icogelb  10625  flqeqceilz  10680  modqadd1  10723  modqmul1  10739  frecuzrdgtcl  10774  frecuzrdgfunlem  10781  fzfig  10792  seqf1og  10883  m1expeven  10948  qsqeqor  11012  fundm2domnop0  11220  ccatrcl1  11302  pfxsuff1eqwrdeq  11391  wrdind  11414  wrd2ind  11415  swrdccat3blem  11431  caucvgrelemcau  11665  rexico  11906  fisumss  12078  fsum2dlemstep  12120  ntrivcvgap  12234  fprodssdc  12276  fprod2dlemstep  12308  0dvds  12497  alzdvds  12540  opoe  12581  omoe  12582  opeo  12583  omeo  12584  m1exp1  12587  nn0enne  12588  nn0o1gt2  12591  gcdneg  12678  dfgcd2  12710  algcvgblem  12746  algcvga  12748  eucalglt  12754  coprmdvds  12789  divgcdcoprmex  12799  cncongr1  12800  prm2orodd  12823  prm23lt5  12961  pockthi  13056  f1ocpbl  13524  f1ovscpbl  13525  f1olecpbl  13526  ismnddef  13631  lmodfopnelem1  14472  tg2  14925  tgcl  14929  neii1  15012  neii2  15014  txlm  15144  reopnap  15411  tgioo  15419  addcncntoplem  15426  gausslemma2dlem0i  15930  2lgslem2  15965  2lgs  15977  2lgsoddprmlem3  15984  uhgr0vb  16079  umgredg  16140  uspgrushgr  16175  uspgrupgr  16176  usgruspgr  16178  uhgr2edg  16201  edg0usgr  16242  egrsubgr  16258  0uhgrsubgr  16260  uhgrspansubgrlem  16271  vtxdg0v  16289  wlkpropg  16319  wlkv  16321  wlkvg  16323  wlkvtxeledgg  16339  wlkl1loop  16353  upgrwlkedg  16356  upgrwlkvtxedg  16359  uspgr2wlkeq  16360  wlkv0  16364  clwwlkccat  16396  clwwlknp  16412  clwwlkext2edg  16417  eupth2lem3lem4fi  16468  bj-elssuniab  16563  bj-nn0sucALT  16748  triap  16813