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  3255  reuanid  3330  rmoanid  3331  axrep5  5198  elinintrab  39944  2sb5nd  40901  eelTT1  41051  uun121  41124  uunTT1  41134  uunTT1p1  41135  uunTT1p2  41136  uun111  41146  uun2221  41154  uun2221p1  41155  uun2221p2  41156  2sb5ndVD  41251  2sb5ndALT  41273