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

Theorem simp1l2 1099
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simp1l2  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta  /\  et )  ->  ps )

Proof of Theorem simp1l2
StepHypRef Expression
1 simpl2 1009 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ps )
213ad2ant1 1026 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta  /\  et )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  mapxpen  7735  lsmcv  18292  pmatcollpw2  19726  btwnconn1lem4  30668  linethru  30731  hlrelat3  32715  cvrval3  32716  cvrval4N  32717  2atlt  32742  atbtwnex  32751  1cvratlt  32777  atcvrlln2  32822  atcvrlln  32823  2llnmat  32827  lvolnlelpln  32888  lnjatN  33083  lncmp  33086  cdlemd9  33510  dihord5b  34565  dihmeetALTN  34633  mapdrvallem2  34951
  Copyright terms: Public domain W3C validator