![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > anassrs | Unicode version |
Description: Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by NM, 15-Nov-2002.) |
Ref | Expression |
---|---|
anassrs.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
anassrs |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | anassrs.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | exp32 358 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | imp31 253 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem is referenced by: anass 394 mpanr1 429 anass1rs 539 anabss5 546 anabss7 551 2ralbida 2400 2rexbidva 2402 pofun 4148 issod 4155 imainss 4860 fvelimab 5373 eqfnfv2 5412 funconstss 5431 fnex 5533 rexima 5548 ralima 5549 f1elima 5566 fliftfun 5589 isores2 5606 isosolem 5617 f1oiso 5619 ovmpt2dxf 5784 grpridd 5855 tfrlemibxssdm 6106 oav2 6238 omv2 6240 nnaass 6260 eroveu 6397 prarloclem4 7118 genpml 7137 genpmu 7138 genpassl 7144 genpassu 7145 prmuloc2 7187 addcomprg 7198 mulcomprg 7200 ltaddpr 7217 ltexprlemloc 7227 addcanprlemu 7235 recexgt0sr 7380 reapmul1 8133 apreim 8141 recexaplem2 8182 creur 8480 uz11 9102 fzrevral 9580 iseqcaopr2 9972 expnlbnd2 10140 shftlem 10311 resqrexlemgt0 10514 cau3lem 10608 clim2 10732 clim2c 10733 clim0c 10735 2clim 10750 climabs0 10757 climcn1 10758 climcn2 10759 climsqz 10784 climsqz2 10785 isummolem2 10833 fsum2dlemstep 10889 fsumiun 10932 mertenslem2 10991 mertensabs 10992 gcdmultiplez 11349 dvdssq 11359 lcmgcdlem 11398 lcmdvds 11400 coprmdvds2 11414 elcncf2 11903 mulc1cncf 11918 cncfco 11920 |
Copyright terms: Public domain | W3C validator |