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

Theorem syl31anc 1220
 Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
sylXanc.1
sylXanc.2
sylXanc.3
sylXanc.4
syl31anc.5
Assertion
Ref Expression
syl31anc

Proof of Theorem syl31anc
StepHypRef Expression
1 sylXanc.1 . . 3
2 sylXanc.2 . . 3
3 sylXanc.3 . . 3
41, 2, 33jca 1162 . 2
5 sylXanc.4 . 2
6 syl31anc.5 . 2
74, 5, 6syl2anc 409 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 103   w3a 963 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107 This theorem depends on definitions:  df-bi 116  df-3an 965 This theorem is referenced by:  syl32anc  1225  stoic4b  1410  enq0tr  7265  ltmul12a  8641  lt2msq1  8666  ledivp1  8684  lemul1ad  8720  lemul2ad  8721  lediv2ad  9535  xaddge0  9690  difelfznle  9942  expubnd  10380  expcanlem  10492  expcand  10494  xrmaxaddlem  11060  mertenslemi1  11335  eftlub  11431  dvdsadd  11570  divalgmod  11658  gcdzeq  11744  rplpwr  11749  sqgcd  11751  bezoutr  11754  rpmulgcd2  11810  rpdvds  11814  divgcdodd  11855  oddpwdclemxy  11881  divnumden  11908  crth  11934  phimullem  11935  xblss2ps  12610  xblss2  12611  metcnpi3  12723  limcimolemlt  12839  limccnp2cntop  12852  dvmulxxbr  12872  dvcoapbr  12877
 Copyright terms: Public domain W3C validator