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  3392  reuanidOLD  3393  axrep5  5287  elinintrab  43590  2sb5nd  44580  eelTT1  44730  uun121  44803  uunTT1  44813  uunTT1p1  44814  uunTT1p2  44815  uun111  44825  uun2221  44833  uun2221p1  44834  uun2221p2  44835  2sb5ndVD  44930  2sb5ndALT  44952
  Copyright terms: Public domain W3C validator