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 362 | . 2 |
3 | 2 | imp31 254 | 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 is referenced by: anass 398 mpanr1 433 anass1rs 545 anabss5 552 anabss7 557 2ralbida 2433 2rexbidva 2435 ralimdvva 2478 pofun 4204 issod 4211 imainss 4924 fvelimab 5445 eqfnfv2 5487 funconstss 5506 fnex 5610 rexima 5624 ralima 5625 f1elima 5642 fliftfun 5665 isores2 5682 isosolem 5693 f1oiso 5695 ovmpodxf 5864 grpridd 5935 tfrlemibxssdm 6192 oav2 6327 omv2 6329 nnaass 6349 eroveu 6488 prarloclem4 7274 genpml 7293 genpmu 7294 genpassl 7300 genpassu 7301 prmuloc2 7343 addcomprg 7354 mulcomprg 7356 ltaddpr 7373 ltexprlemloc 7383 addcanprlemu 7391 recexgt0sr 7549 reapmul1 8324 apreim 8332 recexaplem2 8380 creur 8681 uz11 9304 xaddass 9607 xleadd1a 9611 xlt2add 9618 fzrevral 9840 seq3caopr2 10210 expnlbnd2 10372 shftlem 10543 resqrexlemgt0 10747 cau3lem 10841 clim2 11007 clim2c 11008 clim0c 11010 2clim 11025 climabs0 11031 climcn1 11032 climcn2 11033 climsqz 11059 climsqz2 11060 summodclem2 11106 fsum2dlemstep 11158 fsumiun 11201 mertenslem2 11260 mertensabs 11261 gcdmultiplez 11621 dvdssq 11631 lcmgcdlem 11670 lcmdvds 11672 coprmdvds2 11686 neipsm 12234 lmbrf 12295 lmss 12326 txbas 12338 txbasval 12347 tx1cn 12349 txlm 12359 isxmet2d 12428 elmopn2 12529 mopni3 12564 blsscls2 12573 metequiv2 12576 metss2lem 12577 metrest 12586 metcnp 12592 metcnp2 12593 metcnpi3 12597 elcncf2 12641 mulc1cncf 12656 cncfco 12658 cncfmet 12659 |
Copyright terms: Public domain | W3C validator |