![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > anabs5 | Structured version Visualization version GIF version |
Description: Absorption into embedded conjunct. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 9-Dec-2012.) |
Ref | Expression |
---|---|
anabs5 | ⊢ ((𝜑 ∧ (𝜑 ∧ 𝜓)) ↔ (𝜑 ∧ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ibar 532 | . . 3 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓))) | |
2 | 1 | bicomd 226 | . 2 ⊢ (𝜑 → ((𝜑 ∧ 𝜓) ↔ 𝜓)) |
3 | 2 | pm5.32i 578 | 1 ⊢ ((𝜑 ∧ (𝜑 ∧ 𝜓)) ↔ (𝜑 ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 ∧ wa 399 |
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 210 df-an 400 |
This theorem is referenced by: reuanid 3286 rmoanid 3287 axrep5 5160 elinintrab 40277 2sb5nd 41266 eelTT1 41416 uun121 41489 uunTT1 41499 uunTT1p1 41500 uunTT1p2 41501 uun111 41511 uun2221 41519 uun2221p1 41520 uun2221p2 41521 2sb5ndVD 41616 2sb5ndALT 41638 |
Copyright terms: Public domain | W3C validator |