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

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

Proof of Theorem simp1ll
StepHypRef Expression
1 simpll 730 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  ph )
213ad2ant1 976 1  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th  /\  ta )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  lspsolvlem  15911  dvmptfsum  19338  aannenlem1  19724  measinblem  23562  ax5seg  24638  btwnconn1lem2  24783  btwnconn1lem13  24794  stoweidlem31  27883  stoweidlem34  27886  stoweidlem49  27901  stoweidlem57  27909  athgt  30267  llnle  30329  lplnle  30351  lhpexle1  30819  lhpj1  30833  lhpat3  30857  ltrncnv  30957  cdleme16aN  31070  tendoicl  31607  cdlemk55b  31771  dihatexv  32150  dihglblem6  32152
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  df-3an 936
  Copyright terms: Public domain W3C validator