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

Theorem syl6bi 156
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 136 . 2 (𝜑 → (𝜓𝜒))
3 syl6bi.2 . 2 (𝜒𝜃)
42, 3syl6 33 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  19.33bdc  1537  ax11i  1618  equveli  1658  eupickbi  1998  rgen2a  2392  reu6  2752  sseq0  3285  disjel  3301  disjpss  3305  preq12b  3568  prel12  3569  prneimg  3572  elinti  3651  opthreg  4307  elreldm  4587  issref  4734  relcnvtr  4867  relresfld  4874  funopg  4961  funimass2  5004  fvimacnv  5309  elunirn  5432  oprabid  5564  op1steq  5832  f1o2ndf1  5876  reldmtpos  5898  rntpos  5902  nntri3or  6102  nnaordex  6130  nnawordex  6131  findcard2  6376  findcard2s  6377  lt2addnq  6559  lt2mulnq  6560  genpelvl  6667  genpelvu  6668  distrlem5prl  6741  distrlem5pru  6742  caucvgprlemnkj  6821  rereceu  7020  ltxrlt  7143  0mnnnnn0  8270  elnnnn0b  8282  btwnz  8415  uz11  8590  nn01to3  8648  zq  8657  xrltso  8817  xltnegi  8848  iccleub  8900  fzdcel  9005  uznfz  9066  2ffzeq  9099  elfzonlteqm1  9167  flqeqceilz  9267  modqadd1  9310  modqmul1  9326  frecuzrdgfn  9361  fzfig  9369  m1expeven  9466  caucvgrelemcau  9806  0dvds  10127  alzdvds  10165  opoe  10206  omoe  10207  opeo  10208  omeo  10209  m1exp1  10212  nn0enne  10213  nn0o1gt2  10216  algcvgblem  10250  ialgcvga  10252  bj-elssuniab  10296  bj-nn0sucALT  10469
  Copyright terms: Public domain W3C validator