![]() |
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 3444 onint 7160 f1oweALT 7317 php2 8310 hasheqf1oi 13334 rtrclreclem3 13999 rtrclreclem4 14000 ptcmpfi 21818 redwlk 26779 frgruhgr0v 27417 finxpreclem2 33538 finxpreclem6 33544 diophin 37838 diophun 37839 rspcegf 39681 stoweidlem36 40756 |
Copyright terms: Public domain | W3C validator |