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

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
StepHypRef Expression
1 ibar 529 . . 3 (𝜑 → (𝜓 ↔ (𝜑𝜓)))
21bicomd 224 . 2 (𝜑 → ((𝜑𝜓) ↔ 𝜓))
32pm5.32i 575 1 ((𝜑 ∧ (𝜑𝜓)) ↔ (𝜑𝜓))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 207   ∧ wa 396 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 208  df-an 397 This theorem is referenced by:  rexanidOLD  3258  reuanid  3333  rmoanid  3334  axrep5  5193  elinintrab  39821  2sb5nd  40778  eelTT1  40928  uun121  41001  uunTT1  41011  uunTT1p1  41012  uunTT1p2  41013  uun111  41023  uun2221  41031  uun2221p1  41032  uun2221p2  41033  2sb5ndVD  41128  2sb5ndALT  41150
 Copyright terms: Public domain W3C validator