Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > syl6an | Unicode version |
Description: A syllogism deduction combined with conjoining antecedents. (Contributed by Alan Sare, 28-Oct-2011.) |
Ref | Expression |
---|---|
syl6an.1 | |
syl6an.2 | |
syl6an.3 |
Ref | Expression |
---|---|
syl6an |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl6an.2 | . . 3 | |
2 | syl6an.1 | . . 3 | |
3 | 1, 2 | jctild 314 | . 2 |
4 | syl6an.3 | . 2 | |
5 | 3, 4 | syl6 33 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 107 |
This theorem is referenced by: mapxpen 6793 prarloclem5 7420 ltsopr 7516 suplocsrlem 7728 nominpos 9070 ublbneg 9522 absle 10989 rexanre 11120 rexico 11121 climshftlemg 11199 serf0 11249 dvds1lem 11698 dvds2lem 11699 lmconst 12627 addcncntoplem 12962 bj-indind 13518 |
Copyright terms: Public domain | W3C validator |