Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > syl2an2 | Unicode version |
Description: syl2an 287 with antecedents in standard conjunction form. (Contributed by Alan Sare, 27-Aug-2016.) |
Ref | Expression |
---|---|
syl2an2.1 | |
syl2an2.2 | |
syl2an2.3 |
Ref | Expression |
---|---|
syl2an2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl2an2.1 | . . 3 | |
2 | syl2an2.2 | . . 3 | |
3 | syl2an2.3 | . . 3 | |
4 | 1, 2, 3 | syl2an 287 | . 2 |
5 | 4 | anabss7 573 | 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-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: mapsnf1o 6694 xposdif 9809 qbtwnz 10177 seq3f1o 10429 exp3vallem 10446 fihashf1rn 10691 xrmin2inf 11195 sumrbdclem 11304 summodclem3 11307 zsumdc 11311 fsum3cvg2 11321 mertenslem2 11463 mertensabs 11464 prodrbdclem 11498 prodmodclem2a 11503 zproddc 11506 eftcl 11581 divalgmod 11849 gcdsupex 11875 gcdsupcl 11876 cncongr2 12015 isprm3 12029 eulerthlemrprm 12140 eulerthlema 12141 pcmptdvds 12254 nninfself 13734 |
Copyright terms: Public domain | W3C validator |