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

Theorem anabs5 784
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 490 . . 3  |-  ( ph  ->  ( ps  <->  ( ph  /\ 
ps ) ) )
21bicomd 192 . 2  |-  ( ph  ->  ( ( ph  /\  ps )  <->  ps ) )
32pm5.32i 618 1  |-  ( (
ph  /\  ( ph  /\ 
ps ) )  <->  ( ph  /\ 
ps ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358
This theorem is referenced by:  axrep5  4136  axsep2  4142  2sb5nd  28326  eelTT1  28488  uun121  28558  uunTT1  28568  uunTT1p1  28569  uunTT1p2  28570  uun111  28580  uun2221  28588  uun2221p1  28589  uun2221p2  28590  2sb5ndVD  28686  2sb5ndALT  28709
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 177  df-an 360
  Copyright terms: Public domain W3C validator