![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > anasss | GIF 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 364 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | imp32 257 | 1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem is referenced by: anass 401 anabss3 585 biadanid 614 wepo 4377 wetrep 4378 fvun1 5603 f1elima 5795 caovimo 6090 supisoti 7039 prarloc 7532 reapmul1 8582 ltmul12a 8847 peano5uzti 9391 eluzp1m1 9581 lbzbi 9646 qreccl 9672 xrlttr 9825 xrltso 9826 elfzodifsumelfzo 10231 mertensabs 11577 ndvdsadd 11968 nn0seqcvgd 12073 isprm3 12150 ennnfonelemim 12475 grppropd 12962 ghmcmn 13265 neissex 14122 lgsval3 14877 |
Copyright terms: Public domain | W3C validator |