Theorem anabs5 659

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

Syntax hints:   ↔ wb 205   ∧ wa 394

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 395

This theorem is referenced by:  rmoanidOLD  3386  reuanidOLD  3387  axrep5  5290  elinintrab  42630  2sb5nd  43623  eelTT1  43773  uun121  43846  uunTT1  43856  uunTT1p1  43857  uunTT1p2  43858  uun111  43868  uun2221  43876  uun2221p1  43877  uun2221p2  43878  2sb5ndVD  43973  2sb5ndALT  43995