![]() |
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 528 | . . 3 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓))) | |
2 | 1 | bicomd 223 | . 2 ⊢ (𝜑 → ((𝜑 ∧ 𝜓) ↔ 𝜓)) |
3 | 2 | pm5.32i 574 | 1 ⊢ ((𝜑 ∧ (𝜑 ∧ 𝜓)) ↔ (𝜑 ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 206 ∧ 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: rmoanidOLD 3389 reuanidOLD 3390 axrep5 5292 elinintrab 43566 2sb5nd 44557 eelTT1 44707 uun121 44780 uunTT1 44790 uunTT1p1 44791 uunTT1p2 44792 uun111 44802 uun2221 44810 uun2221p1 44811 uun2221p2 44812 2sb5ndVD 44907 2sb5ndALT 44929 |
Copyright terms: Public domain | W3C validator |