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

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

Proof of Theorem simp123
StepHypRef Expression
1 simp23 990 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )  /\  ta )  ->  ch )
213ad2ant1 976 1  |-  ( ( ( th  /\  ( ph  /\  ps  /\  ch )  /\  ta )  /\  et  /\  ze )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  ax5seglem3  24631  axpasch  24641  exatleN  30215  ps-2b  30293  3atlem1  30294  3atlem2  30295  3atlem4  30297  3atlem5  30298  3atlem6  30299  2llnjaN  30377  2llnjN  30378  4atlem12b  30422  2lplnja  30430  2lplnj  30431  dalemrea  30439  dath2  30548  lneq2at  30589  osumcllem7N  30773  cdleme26ee  31171  cdlemg35  31524  cdlemg36  31525  cdlemj1  31632  cdlemk23-3  31713  cdlemk25-3  31715  cdlemk26b-3  31716  cdlemk27-3  31718  cdlemk28-3  31719  cdleml3N  31789
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator