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

Theorem simp1l3 1100
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 1010 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ch )
213ad2ant1 1026 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta  /\  et )  ->  ch )
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:  btwnconn1lem7  30846  btwnconn1lem12  30851  linethru  30906  hlrelat3  32890  cvrval3  32891  2atlt  32917  atbtwnex  32926  1cvratlt  32952  2llnmat  33002  lplnexllnN  33042  4atlem11  33087  lnjatN  33258  lncvrat  33260  lncmp  33261  cdlemd9  33685  dihord5b  34740  dihmeetALTN  34808  dih1dimatlem0  34809  mapdrvallem2  35126
  Copyright terms: Public domain W3C validator