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

Theorem simp1l2 1082
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 992 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ps )
213ad2ant1 1009 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta  /\  et )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 967
This theorem is referenced by:  mapxpen  7489  lsmcv  17234  btwnconn1lem4  28133  linethru  28196  hlrelat3  33068  cvrval3  33069  cvrval4N  33070  2atlt  33095  atbtwnex  33104  1cvratlt  33130  atcvrlln2  33175  atcvrlln  33176  2llnmat  33180  lvolnlelpln  33241  lnjatN  33436  lncmp  33439  cdlemd9  33862  dihord5b  34916  dihmeetALTN  34984  mapdrvallem2  35302
  Copyright terms: Public domain W3C validator