MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  anabs5 Structured version   Visualization version   GIF version

Theorem anabs5 663
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
StepHypRef Expression
1 ibar 528 . . 3 (𝜑 → (𝜓 ↔ (𝜑𝜓)))
21bicomd 223 . 2 (𝜑 → ((𝜑𝜓) ↔ 𝜓))
32pm5.32i 574 1 ((𝜑 ∧ (𝜑𝜓)) ↔ (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395
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 207  df-an 396
This theorem is referenced by:  rmoanidOLD  3389  reuanidOLD  3390  axrep5  5292  elinintrab  43566  2sb5nd  44557  eelTT1  44707  uun121  44780  uunTT1  44790  uunTT1p1  44791  uunTT1p2  44792  uun111  44802  uun2221  44810  uun2221p1  44811  uun2221p2  44812  2sb5ndVD  44907  2sb5ndALT  44929
  Copyright terms: Public domain W3C validator