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 361 | . 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 398 anabss3 574 wepo 4276 wetrep 4277 fvun1 5480 f1elima 5667 caovimo 5957 supisoti 6890 prarloc 7304 reapmul1 8350 ltmul12a 8611 peano5uzti 9152 eluzp1m1 9342 lbzbi 9401 qreccl 9427 xrlttr 9574 xrltso 9575 elfzodifsumelfzo 9971 mertensabs 11299 ndvdsadd 11617 nn0seqcvgd 11711 isprm3 11788 ennnfonelemim 11926 neissex 12323 |
Copyright terms: Public domain | W3C validator |