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 6742 prarloclem5 7311 ltsopr 7407 suplocsrlem 7619 nominpos 8960 ublbneg 9408 absle 10864 rexanre 10995 rexico 10996 climshftlemg 11074 serf0 11124 dvds1lem 11507 dvds2lem 11508 lmconst 12388 addcncntoplem 12723 bj-indind 13133 |
Copyright terms: Public domain | W3C validator |