New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE 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 588 | . 2 |
3 | 2 | imp31 421 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 358 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 |
This theorem depends on definitions: df-bi 177 df-an 360 |
This theorem is referenced by: anass 630 mpanr1 664 pm2.61ddan 767 pm2.61dda 768 anass1rs 782 anabss5 789 anabss7 794 pm2.61da2ne 2595 2ralbida 2653 2rexbidva 2655 dfimafn 5366 funimass4 5368 eqfnfv2 5393 f1elima 5474 isores2 5493 isomin 5496 f1oiso 5499 weds 5938 |
Copyright terms: Public domain | W3C validator |