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

Theorem simp1l2 1052
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 962 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ps )
213ad2ant1 979 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta  /\  et )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  mapxpen  7274  lsmcv  16214  btwnconn1lem4  26025  linethru  26088  hlrelat3  30210  cvrval3  30211  cvrval4N  30212  2atlt  30237  atbtwnex  30246  1cvratlt  30272  atcvrlln2  30317  atcvrlln  30318  2llnmat  30322  lvolnlelpln  30383  lnjatN  30578  lncmp  30581  cdlemd9  31004  dihord5b  32058  dihmeetALTN  32126  mapdrvallem2  32444
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator