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  4152  axsep2  4158  2sb5nd  28625  eel0121  28790  eelTT1  28794  uun121  28872  uunTT1  28882  uunTT1p1  28883  uunTT1p2  28884  uun111  28894  uun2221  28902  uun2221p1  28903  uun2221p2  28904  2sb5ndVD  29002  2sb5ndALT  29025
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