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

Theorem simp1l1 1089
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 999 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ph )
213ad2ant1 1017 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta  /\  et )  ->  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:  mapxpen  7680  lsmcv  17570  trisegint  29255  linethru  29380  hlrelat3  34208  cvrval3  34209  cvrval4N  34210  2atlt  34235  atbtwnex  34244  1cvratlt  34270  atcvrlln2  34315  atcvrlln  34316  2llnmat  34320  lplnexllnN  34360  lvolnlelpln  34381  lnjatN  34576  lncvrat  34578  lncmp  34579  cdlemd9  35002  dihord5b  36056  dihmeetALTN  36124  dih1dimatlem0  36125  mapdrvallem2  36442
  Copyright terms: Public domain W3C validator