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

Theorem syl6bi 163
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 144 . 2 (𝜑 → (𝜓𝜒))
3 syl6bi.2 . 2 (𝜒𝜃)
42, 3syl6 33 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff set class
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  1630  ax11i  1714  equveli  1759  eupickbi  2108  nfabdw  2338  rgen2a  2531  reu6  2926  sseq0  3464  disjel  3477  preq12b  3768  prel12  3769  prneimg  3772  elinti  3851  exmidundif  4203  opthreg  4551  elreldm  4848  issref  5006  relcnvtr  5143  relresfld  5153  funopg  5245  funimass2  5289  f0dom0  5404  fvimacnv  5626  elunirn  5760  oprabid  5900  op1steq  6173  f1o2ndf1  6222  reldmtpos  6247  rntpos  6251  nntri3or  6487  nnaordex  6522  nnawordex  6523  findcard2  6882  findcard2s  6883  mkvprop  7149  cc2lem  7243  lt2addnq  7381  lt2mulnq  7382  genpelvl  7489  genpelvu  7490  distrlem5prl  7563  distrlem5pru  7564  caucvgprlemnkj  7643  map2psrprg  7782  rereceu  7866  ltxrlt  8000  0mnnnnn0  9184  elnnnn0b  9196  nn0le2is012  9311  btwnz  9348  uz11  9526  nn01to3  9593  zq  9602  xrltso  9770  xltnegi  9809  xnn0lenn0nn0  9839  xnn0xadd0  9841  iccleub  9905  fzdcel  10013  uznfz  10076  2ffzeq  10114  elfzonlteqm1  10183  icogelb  10239  flqeqceilz  10291  modqadd1  10334  modqmul1  10350  frecuzrdgtcl  10385  frecuzrdgfunlem  10392  fzfig  10403  m1expeven  10540  qsqeqor  10603  caucvgrelemcau  10960  rexico  11201  fisumss  11371  fsum2dlemstep  11413  ntrivcvgap  11527  fprodssdc  11569  fprod2dlemstep  11601  0dvds  11789  alzdvds  11830  opoe  11870  omoe  11871  opeo  11872  omeo  11873  m1exp1  11876  nn0enne  11877  nn0o1gt2  11880  gcdneg  11953  dfgcd2  11985  algcvgblem  12019  algcvga  12021  eucalglt  12027  coprmdvds  12062  divgcdcoprmex  12072  cncongr1  12073  prm2orodd  12096  prm23lt5  12233  pockthi  12326  ismnddef  12698  tg2  13193  tgcl  13197  neii1  13280  neii2  13282  txlm  13412  reopnap  13671  tgioo  13679  addcncntoplem  13684  bj-elssuniab  14165  bj-nn0sucALT  14352  triap  14400
  Copyright terms: Public domain W3C validator