Theorem anabs5 661

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 531	. . 3 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓)))
2	1	bicomd 225	. 2 ⊢ (𝜑 → ((𝜑 ∧ 𝜓) ↔ 𝜓))
3	2	pm5.32i 577	1 ⊢ ((𝜑 ∧ (𝜑 ∧ 𝜓)) ↔ (𝜑 ∧ 𝜓))

Syntax hints:   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  rexanidOLD  3253  reuanid  3328  rmoanid  3329  axrep5  5188  elinintrab  39930  2sb5nd  40887  eelTT1  41037  uun121  41110  uunTT1  41120  uunTT1p1  41121  uunTT1p2  41122  uun111  41132  uun2221  41140  uun2221p1  41141  uun2221p2  41142  2sb5ndVD  41237  2sb5ndALT  41259