![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ancom2s | Unicode version |
Description: Inference commuting a nested conjunction in antecedent. (Contributed by NM, 24-May-2006.) (Proof shortened by Wolf Lammen, 24-Nov-2012.) |
Ref | Expression |
---|---|
an12s.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
ancom2s |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm3.22 265 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | an12s.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | sylan2 286 |
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-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem is referenced by: an42s 589 ordsuc 4561 xpexr2m 5069 f1elima 5771 f1imaeq 5773 isosolem 5822 caovlem2d 6064 2ndconst 6220 isotilem 7002 prarloclem4 7494 mulsub 8354 leltadd 8400 eqord1 8436 divmul24ap 8669 fprodseq 11584 grpidpropdg 12725 cmnpropd 13029 unitpropdg 13248 blcomps 13767 blcom 13768 cxple 14208 cxple3 14212 |
Copyright terms: Public domain | W3C validator |