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

Theorem simp1l1 1050
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 960 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ph )
213ad2ant1 978 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta  /\  et )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  mapxpen  7265  lsmcv  16205  trisegint  25954  linethru  26079  hlrelat3  30136  cvrval3  30137  cvrval4N  30138  2atlt  30163  atbtwnex  30172  1cvratlt  30198  atcvrlln2  30243  atcvrlln  30244  2llnmat  30248  lplnexllnN  30288  lvolnlelpln  30309  lnjatN  30504  lncvrat  30506  lncmp  30507  cdlemd9  30930  dihord5b  31984  dihmeetALTN  32052  dih1dimatlem0  32053  mapdrvallem2  32370
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator