| 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 1250 |
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 983 |
| This theorem is referenced by: syl122anc 1259 tfisi 4635 tfrcllemsucfn 6439 sbthlemi6 7064 sbthlemi8 7066 div32apd 8887 div13apd 8888 expdivapd 10832 swrdsbslen 11119 modfsummodlemstep 11768 pcqmul 12626 pcid 12647 pcneg 12648 pc2dvds 12653 pcz 12655 pcaddlem 12662 pcadd 12663 pcmpt2 12667 pcbc 12674 qexpz 12675 expnprm 12676 ennnfonelemg 12774 ssblex 14903 |
| Copyright terms: Public domain | W3C validator |