![]() |
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 206 df-an 396 |
This theorem is referenced by: anabsi6 667 anabsi8 669 3anidm12 1418 rspce 3601 onint 7782 f1oweALT 7963 php2OLD 9229 hasheqf1oi 14318 rtrclreclem3 15014 rtrclreclem4 15015 ablsimpgfindlem1 20025 ptcmpfi 23637 redwlk 29362 frgruhgr0v 29950 finxpreclem2 36735 finxpreclem6 36741 diophin 41973 diophun 41974 rspcegf 44170 stoweidlem36 45211 |
Copyright terms: Public domain | W3C validator |