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 853 | 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 196 df-an 385 |
This theorem is referenced by: anabsi6 855 anabsi8 857 3anidm12 1375 rspce 3277 onint 6887 f1oweALT 7043 php2 8030 hasheqf1oi 13002 hasheqf1oiOLD 13003 rtrclreclem3 13648 rtrclreclem4 13649 ptcmpfi 21426 redwlk 26136 vdusgraval 26434 finxpreclem2 32403 finxpreclem6 32409 diophin 36354 diophun 36355 rspcegf 38205 rspcef 38267 stoweidlem36 38929 red1wlk 40881 frgruhgr0v 41435 |
Copyright terms: Public domain | W3C validator |