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 6735 prarloclem5 7301 ltsopr 7397 suplocsrlem 7609 nominpos 8950 ublbneg 9398 absle 10854 rexanre 10985 rexico 10986 climshftlemg 11064 serf0 11114 dvds1lem 11493 dvds2lem 11494 lmconst 12374 addcncntoplem 12709 bj-indind 13119 |
Copyright terms: Public domain | W3C validator |