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

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

Proof of Theorem syl122anc
StepHypRef Expression
1 sylXanc.1 . 2
2 sylXanc.2 . 2
3 sylXanc.3 . 2
4 sylXanc.4 . . 3
5 sylXanc.5 . . 3
64, 5jca 304 . 2
7 syl122anc.6 . 2
81, 2, 3, 6, 7syl121anc 1222 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:  divdiv32apd  8596  divcanap5d  8597  divcanap7d  8599  divdivap1d  8602  divdivap2d  8603  seq3coll  10613  cau3lem  10914  summodclem2a  11178  prodmodclem2a  11373  prmind2  11828  divnumden  11901  blss2ps  12605  blss2  12606  blssps  12626  blss  12627  xmeter  12635
 Copyright terms: Public domain W3C validator