ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  syl6bi GIF version

Theorem syl6bi 162
Description: A mixed syllogism inference. (Contributed by NM, 2-Jan-1994.)
Hypotheses
Ref Expression
syl6bi.1 (𝜑 → (𝜓𝜒))
syl6bi.2 (𝜒𝜃)
Assertion
Ref Expression
syl6bi (𝜑 → (𝜓𝜃))

Proof of Theorem syl6bi
StepHypRef Expression
1 syl6bi.1 . . 3 (𝜑 → (𝜓𝜒))
21biimpd 143 . 2 (𝜑 → (𝜓𝜒))
3 syl6bi.2 . 2 (𝜒𝜃)
42, 3syl6 33 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  19.33bdc  1610  ax11i  1693  equveli  1733  eupickbi  2082  rgen2a  2489  reu6  2876  sseq0  3408  disjel  3421  preq12b  3704  prel12  3705  prneimg  3708  elinti  3787  exmidundif  4136  opthreg  4478  elreldm  4772  issref  4928  relcnvtr  5065  relresfld  5075  funopg  5164  funimass2  5208  f0dom0  5323  fvimacnv  5542  elunirn  5674  oprabid  5810  op1steq  6084  f1o2ndf1  6132  reldmtpos  6157  rntpos  6161  nntri3or  6396  nnaordex  6430  nnawordex  6431  findcard2  6790  findcard2s  6791  mkvprop  7039  cc2lem  7097  lt2addnq  7235  lt2mulnq  7236  genpelvl  7343  genpelvu  7344  distrlem5prl  7417  distrlem5pru  7418  caucvgprlemnkj  7497  map2psrprg  7636  rereceu  7720  ltxrlt  7853  0mnnnnn0  9032  elnnnn0b  9044  nn0le2is012  9156  btwnz  9193  uz11  9371  nn01to3  9435  zq  9444  xrltso  9611  xltnegi  9647  xnn0lenn0nn0  9677  xnn0xadd0  9679  iccleub  9743  fzdcel  9850  uznfz  9913  2ffzeq  9948  elfzonlteqm1  10017  flqeqceilz  10121  modqadd1  10164  modqmul1  10180  frecuzrdgtcl  10215  frecuzrdgfunlem  10222  fzfig  10233  m1expeven  10370  caucvgrelemcau  10783  rexico  11024  fisumss  11192  fsum2dlemstep  11234  ntrivcvgap  11348  0dvds  11547  alzdvds  11586  opoe  11626  omoe  11627  opeo  11628  omeo  11629  m1exp1  11632  nn0enne  11633  nn0o1gt2  11636  gcdneg  11704  dfgcd2  11736  algcvgblem  11764  algcvga  11766  eucalglt  11772  coprmdvds  11807  divgcdcoprmex  11817  cncongr1  11818  prm2orodd  11841  tg2  12266  tgcl  12270  neii1  12353  neii2  12355  txlm  12485  reopnap  12744  tgioo  12752  addcncntoplem  12757  bj-elssuniab  13167  bj-nn0sucALT  13345  triap  13397
  Copyright terms: Public domain W3C validator