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

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

Proof of Theorem simp1l3
StepHypRef Expression
1 simpl3 962 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ch )
213ad2ant1 978 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta  /\  et )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  btwnconn1lem7  26027  btwnconn1lem12  26032  linethru  26087  hlrelat3  30209  cvrval3  30210  2atlt  30236  atbtwnex  30245  1cvratlt  30271  2llnmat  30321  lplnexllnN  30361  4atlem11  30406  lnjatN  30577  lncvrat  30579  lncmp  30580  cdlemd9  31003  dihord5b  32057  dihmeetALTN  32125  dih1dimatlem0  32126  mapdrvallem2  32443
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