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

Theorem simp1ll 1021
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 732 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  ph )
213ad2ant1 979 1  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th  /\  ta )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  lspsolvlem  16216  measinblem  24576  ax5seg  25879  btwnconn1lem2  26024  btwnconn1lem13  26035  stoweidlem31  27758  stoweidlem34  27761  stoweidlem49  27776  stoweidlem57  27784  athgt  30315  llnle  30377  lplnle  30399  lhpexle1  30867  lhpj1  30881  lhpat3  30905  ltrncnv  31005  cdleme16aN  31118  tendoicl  31655  cdlemk55b  31819  dihatexv  32198  dihglblem6  32200
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