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  15895  dvmptfsum  19322  aannenlem1  19708  measinblem  23547  ax5seg  24566  btwnconn1lem2  24711  btwnconn1lem13  24722  stoweidlem31  27780  stoweidlem34  27783  stoweidlem49  27798  stoweidlem57  27806  athgt  29645  llnle  29707  lplnle  29729  lhpexle1  30197  lhpj1  30211  lhpat3  30235  ltrncnv  30335  cdleme16aN  30448  tendoicl  30985  cdlemk55b  31149  dihatexv  31528  dihglblem6  31530
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