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

Theorem simp1l3 1083
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 993 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ch )
213ad2ant1 1009 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta  /\  et )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 371  df-3an 967
This theorem is referenced by:  btwnconn1lem7  28124  btwnconn1lem12  28129  linethru  28184  hlrelat3  33056  cvrval3  33057  2atlt  33083  atbtwnex  33092  1cvratlt  33118  2llnmat  33168  lplnexllnN  33208  4atlem11  33253  lnjatN  33424  lncvrat  33426  lncmp  33427  cdlemd9  33850  dihord5b  34904  dihmeetALTN  34972  dih1dimatlem0  34973  mapdrvallem2  35290
  Copyright terms: Public domain W3C validator