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

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

Proof of Theorem simp122
StepHypRef Expression
1 simp22 989 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )  /\  ta )  ->  ps )
213ad2ant1 976 1  |-  ( ( ( th  /\  ( ph  /\  ps  /\  ch )  /\  ta )  /\  et  /\  ze )  ->  ps )
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  4atlem12b  30422  2lplnja  30430  dalemqea  30438  dath2  30548  lneq2at  30589  llnexchb2  30680  dalawlem1  30682  lhpexle3lem  30822  cdleme26ee  31171  cdlemg34  31523  cdlemg35  31524  cdlemg36  31525  cdlemj1  31632  cdlemj2  31633  cdlemk23-3  31713  cdlemk25-3  31715  cdlemk26b-3  31716  cdlemk26-3  31717  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