Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > anasss | Unicode version |
Description: Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by NM, 15-Nov-2002.) |
Ref | Expression |
---|---|
anasss.1 |
Ref | Expression |
---|---|
anasss |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | anasss.1 | . . 3 | |
2 | 1 | exp31 362 | . 2 |
3 | 2 | imp32 255 | 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 399 anabss3 580 wepo 4344 wetrep 4345 fvun1 5562 f1elima 5752 caovimo 6046 supisoti 6987 prarloc 7465 reapmul1 8514 ltmul12a 8776 peano5uzti 9320 eluzp1m1 9510 lbzbi 9575 qreccl 9601 xrlttr 9752 xrltso 9753 elfzodifsumelfzo 10157 mertensabs 11500 ndvdsadd 11890 nn0seqcvgd 11995 isprm3 12072 ennnfonelemim 12379 grppropd 12724 neissex 12959 lgsval3 13713 |
Copyright terms: Public domain | W3C validator |