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

Theorem simp1l2 1090
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simp1l2  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta  /\  et )  ->  ps )

Proof of Theorem simp1l2
StepHypRef Expression
1 simpl2 1000 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ps )
213ad2ant1 1017 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta  /\  et )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973
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 185  df-an 371  df-3an 975
This theorem is referenced by:  mapxpen  7683  lsmcv  17582  pmatcollpw2  19062  btwnconn1lem4  29333  linethru  29396  hlrelat3  34217  cvrval3  34218  cvrval4N  34219  2atlt  34244  atbtwnex  34253  1cvratlt  34279  atcvrlln2  34324  atcvrlln  34325  2llnmat  34329  lvolnlelpln  34390  lnjatN  34585  lncmp  34588  cdlemd9  35011  dihord5b  36065  dihmeetALTN  36133  mapdrvallem2  36451
  Copyright terms: Public domain W3C validator