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

Theorem anabs5 785
Description: Absorption into embedded conjunct. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 9-Dec-2012.)
Assertion
Ref Expression
anabs5  |-  ( (
ph  /\  ( ph  /\ 
ps ) )  <->  ( ph  /\ 
ps ) )

Proof of Theorem anabs5
StepHypRef Expression
1 ibar 491 . . 3  |-  ( ph  ->  ( ps  <->  ( ph  /\ 
ps ) ) )
21bicomd 193 . 2  |-  ( ph  ->  ( ( ph  /\  ps )  <->  ps ) )
32pm5.32i 619 1  |-  ( (
ph  /\  ( ph  /\ 
ps ) )  <->  ( ph  /\ 
ps ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359
This theorem is referenced by:  axrep5  4325  axsep2  4331  2sb5nd  28647  eelTT1  28817  uun121  28895  uunTT1  28905  uunTT1p1  28906  uunTT1p2  28907  uun111  28917  uun2221  28925  uun2221p1  28926  uun2221p2  28927  2sb5ndVD  29022  2sb5ndALT  29044
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator