| 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 3392 reuanidOLD 3393 axrep5 5287 elinintrab 43590 2sb5nd 44580 eelTT1 44730 uun121 44803 uunTT1 44813 uunTT1p1 44814 uunTT1p2 44815 uun111 44825 uun2221 44833 uun2221p1 44834 uun2221p2 44835 2sb5ndVD 44930 2sb5ndALT 44952 |
| Copyright terms: Public domain | W3C validator |