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

Theorem simp1ll 1062
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 754 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  ph )
213ad2ant1 1020 1  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th  /\  ta )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 976
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 187  df-an 371  df-3an 978
This theorem is referenced by:  lspsolvlem  18110  1marepvsma1  19379  mdetunilem8  19415  madutpos  19438  ax5seg  24670  rabfodom  27832  measinblem  28681  btwnconn1lem2  30439  btwnconn1lem13  30450  athgt  32486  llnle  32548  lplnle  32570  lhpexle1  33038  lhpj1  33052  lhpat3  33076  ltrncnv  33176  cdleme16aN  33290  tendoicl  33828  cdlemk55b  33992  dihatexv  34371  dihglblem6  34373  limccog  37007  icccncfext  37071  stoweidlem31  37194  stoweidlem34  37197  stoweidlem49  37212  stoweidlem57  37220
  Copyright terms: Public domain W3C validator