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

Theorem simp1l3 1092
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 1002 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ch )
213ad2ant1 1018 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta  /\  et )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 974
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 976
This theorem is referenced by:  btwnconn1lem7  30404  btwnconn1lem12  30409  linethru  30464  hlrelat3  32410  cvrval3  32411  2atlt  32437  atbtwnex  32446  1cvratlt  32472  2llnmat  32522  lplnexllnN  32562  4atlem11  32607  lnjatN  32778  lncvrat  32780  lncmp  32781  cdlemd9  33205  dihord5b  34260  dihmeetALTN  34328  dih1dimatlem0  34329  mapdrvallem2  34646
  Copyright terms: Public domain W3C validator