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

Theorem simp1ll 1059
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 1017 1  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th  /\  ta )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973
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 975
This theorem is referenced by:  lspsolvlem  17571  1marepvsma1  18852  mdetunilem8  18888  madutpos  18911  ax5seg  23917  measinblem  27831  btwnconn1lem2  29315  btwnconn1lem13  29326  limccog  31162  icccncfext  31226  stoweidlem31  31331  stoweidlem34  31334  stoweidlem49  31349  stoweidlem57  31357  athgt  34252  llnle  34314  lplnle  34336  lhpexle1  34804  lhpj1  34818  lhpat3  34842  ltrncnv  34942  cdleme16aN  35055  tendoicl  35592  cdlemk55b  35756  dihatexv  36135  dihglblem6  36137
  Copyright terms: Public domain W3C validator