![]() |
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 316 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | syl6an.3 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | syl6 33 |
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-ia3 108 |
This theorem is referenced by: mapxpen 6847 prarloclem5 7498 ltsopr 7594 suplocsrlem 7806 nominpos 9155 ublbneg 9612 absle 11097 rexanre 11228 rexico 11229 climshftlemg 11309 serf0 11359 dvds1lem 11808 dvds2lem 11809 lmconst 13686 addcncntoplem 14021 bj-indind 14654 |
Copyright terms: Public domain | W3C validator |