![]() |
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 397 | . 2 ⊢ ((𝜑 ∧ (𝜑 ∧ 𝜓)) → 𝜒) |
3 | 2 | anabss5 658 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 |
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 199 df-an 387 |
This theorem is referenced by: anabsi6 660 anabsi8 662 3anidm12 1491 rspce 3506 onint 7275 f1oweALT 7431 php2 8435 hasheqf1oi 13463 rtrclreclem3 14213 rtrclreclem4 14214 ptcmpfi 22036 redwlk 27040 frgruhgr0v 27688 finxpreclem2 33829 finxpreclem6 33835 diophin 38310 diophun 38311 rspcegf 40129 stoweidlem36 41194 |
Copyright terms: Public domain | W3C validator |