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  7043  lsmcv  15910  trisegint  24723  linethru  24848  hlrelat3  30223  cvrval3  30224  cvrval4N  30225  2atlt  30250  atbtwnex  30259  1cvratlt  30285  atcvrlln2  30330  atcvrlln  30331  2llnmat  30335  lplnexllnN  30375  lvolnlelpln  30396  lnjatN  30591  lncvrat  30593  lncmp  30594  cdlemd9  31017  dihord5b  32071  dihmeetALTN  32139  dih1dimatlem0  32140  mapdrvallem2  32457
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