![]() |
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 1418 rspce 3611 onint 7810 f1oweALT 7996 php2OLD 9258 hasheqf1oi 14387 rtrclreclem3 15096 rtrclreclem4 15097 ablsimpgfindlem1 20142 ptcmpfi 23837 redwlk 29705 frgruhgr0v 30293 finxpreclem2 37373 finxpreclem6 37379 diophin 42760 diophun 42761 rspcegf 44961 stoweidlem36 45992 grlimgrtri 47899 |
Copyright terms: Public domain | W3C validator |