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 346 | . 2 |
3 | 2 | imp32 244 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 97 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem is referenced by: anass 381 anabss3 519 wepo 4096 wetrep 4097 fvun1 5239 f1elima 5412 caovimo 5694 prarloc 6601 reapmul1 7586 ltmul12a 7826 peano5uzti 8346 eluzp1m1 8496 lbzbi 8551 qreccl 8576 xrlttr 8716 xrltso 8717 elfzodifsumelfzo 9057 nn0seqcvgd 9880 |
Copyright terms: Public domain | W3C validator |