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

Theorem simp1l1 1081
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 991 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ph )
213ad2ant1 1009 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta  /\  et )  ->  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:  mapxpen  7492  lsmcv  17237  trisegint  28074  linethru  28199  hlrelat3  33075  cvrval3  33076  cvrval4N  33077  2atlt  33102  atbtwnex  33111  1cvratlt  33137  atcvrlln2  33182  atcvrlln  33183  2llnmat  33187  lplnexllnN  33227  lvolnlelpln  33248  lnjatN  33443  lncvrat  33445  lncmp  33446  cdlemd9  33869  dihord5b  34923  dihmeetALTN  34991  dih1dimatlem0  34992  mapdrvallem2  35309
  Copyright terms: Public domain W3C validator