| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > syl121anc | Unicode version | ||
| Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
| Ref | Expression |
|---|---|
| sylXanc.1 |
|
| sylXanc.2 |
|
| sylXanc.3 |
|
| sylXanc.4 |
|
| syl121anc.5 |
|
| Ref | Expression |
|---|---|
| syl121anc |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sylXanc.1 |
. 2
| |
| 2 | sylXanc.2 |
. . 3
| |
| 3 | sylXanc.3 |
. . 3
| |
| 4 | 2, 3 | jca 306 |
. 2
|
| 5 | sylXanc.4 |
. 2
| |
| 6 | syl121anc.5 |
. 2
| |
| 7 | 1, 4, 5, 6 | syl3anc 1249 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
| This theorem depends on definitions: df-bi 117 df-3an 982 |
| This theorem is referenced by: syl122anc 1258 tfisi 4634 tfrcllemsucfn 6438 sbthlemi6 7063 sbthlemi8 7065 div32apd 8886 div13apd 8887 expdivapd 10830 modfsummodlemstep 11739 pcqmul 12597 pcid 12618 pcneg 12619 pc2dvds 12624 pcz 12626 pcaddlem 12633 pcadd 12634 pcmpt2 12638 pcbc 12645 qexpz 12646 expnprm 12647 ennnfonelemg 12745 ssblex 14874 |
| Copyright terms: Public domain | W3C validator |