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

Theorem simp1ll 1051
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 753 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  ph )
213ad2ant1 1009 1  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th  /\  ta )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 967
This theorem is referenced by:  lspsolvlem  17226  1marepvsma1  18397  mdetunilem8  18428  madutpos  18451  ax5seg  23187  measinblem  26637  btwnconn1lem2  28122  btwnconn1lem13  28133  stoweidlem31  29829  stoweidlem34  29832  stoweidlem49  29847  stoweidlem57  29855  athgt  33103  llnle  33165  lplnle  33187  lhpexle1  33655  lhpj1  33669  lhpat3  33693  ltrncnv  33793  cdleme16aN  33906  tendoicl  34443  cdlemk55b  34607  dihatexv  34986  dihglblem6  34988
  Copyright terms: Public domain W3C validator