| 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 | simpl 482 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜑) | |
| 2 | anabsi5.1 | . 2 ⊢ (𝜑 → ((𝜑 ∧ 𝜓) → 𝜒)) | |
| 3 | 1, 2 | mpcom 38 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 |
| 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 207 df-an 396 |
| This theorem is referenced by: anabsi6 670 anabsi8 672 3anidm12 1421 rspce 3611 onint 7810 f1oweALT 7997 php2OLD 9260 hasheqf1oi 14390 rtrclreclem3 15099 rtrclreclem4 15100 ablsimpgfindlem1 20127 ptcmpfi 23821 redwlk 29690 frgruhgr0v 30283 finxpreclem2 37391 finxpreclem6 37397 diophin 42783 diophun 42784 rspcegf 45028 stoweidlem36 46051 grlimgrtri 47963 |
| Copyright terms: Public domain | W3C validator |