MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp1l1 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  7210  lsmcv  16141  trisegint  25677  linethru  25802  hlrelat3  29527  cvrval3  29528  cvrval4N  29529  2atlt  29554  atbtwnex  29563  1cvratlt  29589  atcvrlln2  29634  atcvrlln  29635  2llnmat  29639  lplnexllnN  29679  lvolnlelpln  29700  lnjatN  29895  lncvrat  29897  lncmp  29898  cdlemd9  30321  dihord5b  31375  dihmeetALTN  31443  dih1dimatlem0  31444  mapdrvallem2  31761
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