![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > anabsi5 | Structured version Visualization version GIF version |
Description: Absorption of antecedent into conjunction. (Contributed by NM, 11-Jun-1995.) (Proof shortened by Wolf Lammen, 18-Nov-2013.) |
Ref | Expression |
---|---|
anabsi5.1 | ⊢ (𝜑 → ((𝜑 ∧ 𝜓) → 𝜒)) |
Ref | Expression |
---|---|
anabsi5 | ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | anabsi5.1 | . . 3 ⊢ (𝜑 → ((𝜑 ∧ 𝜓) → 𝜒)) | |
2 | 1 | imp 444 | . 2 ⊢ ((𝜑 ∧ (𝜑 ∧ 𝜓)) → 𝜒) |
3 | 2 | anabss5 892 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 197 df-an 385 |
This theorem is referenced by: anabsi6 894 anabsi8 896 3anidm12 1530 rspce 3445 onint 7162 f1oweALT 7319 php2 8313 hasheqf1oi 13355 rtrclreclem3 14020 rtrclreclem4 14021 ptcmpfi 21839 redwlk 26801 frgruhgr0v 27439 finxpreclem2 33557 finxpreclem6 33563 diophin 37857 diophun 37858 rspcegf 39700 stoweidlem36 40775 |
Copyright terms: Public domain | W3C validator |