![]() |
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 363 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | imp31 254 |
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 105 ax-ia2 106 ax-ia3 107 |
This theorem is referenced by: anass 399 mpanr1 434 anass1rs 561 anabss5 568 anabss7 573 2ralbida 2459 2rexbidva 2461 ralimdvva 2504 pofun 4242 issod 4249 imainss 4962 fvelimab 5485 eqfnfv2 5527 funconstss 5546 fnex 5650 rexima 5664 ralima 5665 f1elima 5682 fliftfun 5705 isores2 5722 isosolem 5733 f1oiso 5735 ovmpodxf 5904 grpridd 5975 tfrlemibxssdm 6232 oav2 6367 omv2 6369 nnaass 6389 eroveu 6528 prarloclem4 7330 genpml 7349 genpmu 7350 genpassl 7356 genpassu 7357 prmuloc2 7399 addcomprg 7410 mulcomprg 7412 ltaddpr 7429 ltexprlemloc 7439 addcanprlemu 7447 recexgt0sr 7605 reapmul1 8381 apreim 8389 recexaplem2 8437 creur 8741 uz11 9372 xaddass 9682 xleadd1a 9686 xlt2add 9693 fzrevral 9916 seq3caopr2 10286 expnlbnd2 10448 shftlem 10620 resqrexlemgt0 10824 cau3lem 10918 clim2 11084 clim2c 11085 clim0c 11087 2clim 11102 climabs0 11108 climcn1 11109 climcn2 11110 climsqz 11136 climsqz2 11137 summodclem2 11183 fsum2dlemstep 11235 fsumiun 11278 mertenslem2 11337 mertensabs 11338 prodfrecap 11347 gcdmultiplez 11745 dvdssq 11755 lcmgcdlem 11794 lcmdvds 11796 coprmdvds2 11810 neipsm 12362 lmbrf 12423 lmss 12454 txbas 12466 txbasval 12475 tx1cn 12477 txlm 12487 isxmet2d 12556 elmopn2 12657 mopni3 12692 blsscls2 12701 metequiv2 12704 metss2lem 12705 metrest 12714 metcnp 12720 metcnp2 12721 metcnpi3 12725 elcncf2 12769 mulc1cncf 12784 cncfco 12786 cncfmet 12787 |
Copyright terms: Public domain | W3C validator |