Theorem anabs5 662

Description: Absorption into embedded conjunct. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 9-Dec-2012.)

Assertion

Ref	Expression
anabs5	⊢ ((𝜑 ∧ (𝜑 ∧ 𝜓)) ↔ (𝜑 ∧ 𝜓))

Proof of Theorem anabs5

Step	Hyp	Ref	Expression
1		ibar 530	. . 3 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓)))
2	1	bicomd 222	. 2 ⊢ (𝜑 → ((𝜑 ∧ 𝜓) ↔ 𝜓))
3	2	pm5.32i 576	1 ⊢ ((𝜑 ∧ (𝜑 ∧ 𝜓)) ↔ (𝜑 ∧ 𝜓))

Syntax hints:   ↔ wb 205   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  rmoanidOLD  3389  reuanidOLD  3390  axrep5  5292  elinintrab  42328  2sb5nd  43321  eelTT1  43471  uun121  43544  uunTT1  43554  uunTT1p1  43555  uunTT1p2  43556  uun111  43566  uun2221  43574  uun2221p1  43575  uun2221p2  43576  2sb5ndVD  43671  2sb5ndALT  43693