![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ancom2s | Structured version Visualization version 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 455 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | an12s.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | sylan2 481 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 190 df-an 377 |
This theorem is referenced by: an42s 841 sotr2 4802 somin2 5253 f1elima 6188 f1imaeq 6190 soisoi 6243 isosolem 6262 xpexr2 6760 2ndconst 6911 smoword 7110 unxpdomlem3 7803 fiming 8039 fiinfg 8040 sornom 8732 fin1a2s 8869 mulsub 10088 leltadd 10125 ltord1 10167 leord1 10168 eqord1 10169 divmul24 10338 expcan 12356 ltexp2 12357 fsum 13834 fprod 14043 isprm5 14699 ramub 15018 setcinv 16033 grpidpropd 16552 gsumpropd2lem 16564 cmnpropd 17487 unitpropd 17973 lidl1el 18490 gsumcom3 19472 1marepvmarrepid 19648 1marepvsma1 19656 ordtrest2 20268 filuni 20948 haustsms2 21199 blcomps 21456 blcom 21457 metnrmlem3 21926 metnrmlem3OLD 21941 cnmpt2pc 22004 icoopnst 22015 icccvx 22026 equivcfil 22317 volcn 22612 dvmptfsum 22975 cxple 23688 cxple3 23694 subgoablo 26087 ghabloOLD 26145 lnosub 26448 chirredlem2 28092 bhmafibid2 28454 metider 28745 ordtrest2NEW 28777 finxpreclem2 31826 fin2so 31976 cover2 32084 filbcmb 32111 isdrngo2 32241 crngohomfo 32283 unichnidl 32308 cdleme50eq 34152 dvhvaddcomN 34708 ismrc 35587 uhgr2edg 39338 |
Copyright terms: Public domain | W3C validator |