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 575 wepo 4319 wetrep 4320 fvun1 5534 f1elima 5723 caovimo 6014 supisoti 6954 prarloc 7423 reapmul1 8470 ltmul12a 8731 peano5uzti 9272 eluzp1m1 9462 lbzbi 9525 qreccl 9551 xrlttr 9702 xrltso 9703 elfzodifsumelfzo 10100 mertensabs 11434 ndvdsadd 11822 nn0seqcvgd 11918 isprm3 11995 ennnfonelemim 12164 neissex 12576 |
Copyright terms: Public domain | W3C validator |