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

Theorem simp1l1 1087
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 997 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ph )
213ad2ant1 1015 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta  /\  et )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 971
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 369  df-3an 973
This theorem is referenced by:  mapxpen  7624  lsmcv  17923  archiabl  27929  trisegint  29871  linethru  29996  hlrelat3  35588  cvrval3  35589  cvrval4N  35590  2atlt  35615  atbtwnex  35624  1cvratlt  35650  atcvrlln2  35695  atcvrlln  35696  2llnmat  35700  lplnexllnN  35740  lvolnlelpln  35761  lnjatN  35956  lncvrat  35958  lncmp  35959  cdlemd9  36383  dihord5b  37438  dihmeetALTN  37506  dih1dimatlem0  37507  mapdrvallem2  37824
  Copyright terms: Public domain W3C validator