Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > syl122anc | Unicode version |
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
Ref | Expression |
---|---|
sylXanc.1 | |
sylXanc.2 | |
sylXanc.3 | |
sylXanc.4 | |
sylXanc.5 | |
syl122anc.6 |
Ref | Expression |
---|---|
syl122anc |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylXanc.1 | . 2 | |
2 | sylXanc.2 | . 2 | |
3 | sylXanc.3 | . 2 | |
4 | sylXanc.4 | . . 3 | |
5 | sylXanc.5 | . . 3 | |
6 | 4, 5 | jca 304 | . 2 |
7 | syl122anc.6 | . 2 | |
8 | 1, 2, 3, 6, 7 | syl121anc 1221 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 w3a 962 |
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 964 |
This theorem is referenced by: divdiv32apd 8576 divcanap5d 8577 divcanap7d 8579 divdivap1d 8582 divdivap2d 8583 seq3coll 10585 cau3lem 10886 summodclem2a 11150 prodmodclem2a 11345 prmind2 11801 divnumden 11874 blss2ps 12575 blss2 12576 blssps 12596 blss 12597 xmeter 12605 |
Copyright terms: Public domain | W3C validator |