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

Theorem simp1l1 1099
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 1009 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ph )
213ad2ant1 1027 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta  /\  et )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    /\ w3a 983
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 189  df-an 373  df-3an 985
This theorem is referenced by:  mapxpen  7742  lsmcv  18357  archiabl  28516  trisegint  30794  linethru  30919  hlrelat3  32940  cvrval3  32941  cvrval4N  32942  2atlt  32967  atbtwnex  32976  1cvratlt  33002  atcvrlln2  33047  atcvrlln  33048  2llnmat  33052  lplnexllnN  33092  lvolnlelpln  33113  lnjatN  33308  lncvrat  33310  lncmp  33311  cdlemd9  33735  dihord5b  34790  dihmeetALTN  34858  dih1dimatlem0  34859  mapdrvallem2  35176
  Copyright terms: Public domain W3C validator