Theorem anabs5 676

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  axrep5  5240  elinintrab  44417  2sb5nd  45383  eelTT1  45532  uun121  45605  uunTT1  45615  uunTT1p1  45616  uunTT1p2  45617  uun111  45627  uun2221  45635  uun2221p1  45636  uun2221p2  45637  2sb5ndVD  45732  2sb5ndALT  45754