![]() |
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 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 4289 wetrep 4290 fvun1 5495 f1elima 5682 caovimo 5972 supisoti 6905 prarloc 7335 reapmul1 8381 ltmul12a 8642 peano5uzti 9183 eluzp1m1 9373 lbzbi 9435 qreccl 9461 xrlttr 9611 xrltso 9612 elfzodifsumelfzo 10009 mertensabs 11338 ndvdsadd 11664 nn0seqcvgd 11758 isprm3 11835 ennnfonelemim 11973 neissex 12373 |
Copyright terms: Public domain | W3C validator |