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

Theorem simp1l1 1048
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simp1l1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta  /\  et )  ->  ph )

Proof of Theorem simp1l1
StepHypRef Expression
1 simpl1 958 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ph )
213ad2ant1 976 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta  /\  et )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  mapxpen  7027  lsmcv  15894  trisegint  24651  linethru  24776  hlrelat3  29601  cvrval3  29602  cvrval4N  29603  2atlt  29628  atbtwnex  29637  1cvratlt  29663  atcvrlln2  29708  atcvrlln  29709  2llnmat  29713  lplnexllnN  29753  lvolnlelpln  29774  lnjatN  29969  lncvrat  29971  lncmp  29972  cdlemd9  30395  dihord5b  31449  dihmeetALTN  31517  dih1dimatlem0  31518  mapdrvallem2  31835
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator