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

Theorem simp1ll 1044
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 746 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  ph )
213ad2ant1 1002 1  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th  /\  ta )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 958
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 960
This theorem is referenced by:  lspsolvlem  17145  1marepvsma1  18236  mdetunilem8  18267  madutpos  18290  ax5seg  23007  measinblem  26488  btwnconn1lem2  27966  btwnconn1lem13  27977  stoweidlem31  29672  stoweidlem34  29675  stoweidlem49  29690  stoweidlem57  29698  athgt  32673  llnle  32735  lplnle  32757  lhpexle1  33225  lhpj1  33239  lhpat3  33263  ltrncnv  33363  cdleme16aN  33476  tendoicl  34013  cdlemk55b  34177  dihatexv  34556  dihglblem6  34558
  Copyright terms: Public domain W3C validator