Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > syl2an2r | Unicode version |
Description: syl2anr 288 with antecedents in standard conjunction form. (Contributed by Alan Sare, 27-Aug-2016.) |
Ref | Expression |
---|---|
syl2an2r.1 | |
syl2an2r.2 | |
syl2an2r.3 |
Ref | Expression |
---|---|
syl2an2r |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl2an2r.1 | . . 3 | |
2 | syl2an2r.2 | . . 3 | |
3 | syl2an2r.3 | . . 3 | |
4 | 1, 2, 3 | syl2an 287 | . 2 |
5 | 4 | anabss5 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: op1stbg 4464 mapen 6824 fival 6947 supelti 6979 supmaxti 6981 infminti 7004 xnegdi 9825 frecuzrdgsuc 10370 hashunlem 10739 2zsupmax 11189 xrmin1inf 11230 serf0 11315 fsumabs 11428 binomlem 11446 cvgratz 11495 efcllemp 11621 ef0lem 11623 tannegap 11691 modm1div 11762 divalglemnqt 11879 lcmid 12034 hashdvds 12175 prmdivdiv 12191 odzcllem 12196 reumodprminv 12207 nnnn0modprm0 12209 pythagtrip 12237 pcmpt 12295 pockthg 12309 4sqlem9 12338 ennnfonelemkh 12367 ctinf 12385 nninfdclemp1 12405 setsslid 12466 grprinvlem 12639 isgrpinv 12756 topbas 12861 tgrest 12963 txss12 13060 cnplimclemle 13431 efltlemlt 13489 coseq0q4123 13549 lgsval 13699 lgscllem 13702 neapmkvlem 14098 |
Copyright terms: Public domain | W3C validator |