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

Theorem simp122 1114
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 1015 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )  /\  ta )  ->  ps )
213ad2ant1 1002 1  |-  ( ( ( th  /\  ( ph  /\  ps  /\  ch )  /\  ta )  /\  et  /\  ze )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 958
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 960
This theorem is referenced by:  ax5seglem3  23000  axpasch  23010  exatleN  32621  ps-2b  32699  3atlem1  32700  3atlem2  32701  3atlem4  32703  3atlem5  32704  3atlem6  32705  2llnjaN  32783  4atlem12b  32828  2lplnja  32836  dalemqea  32844  dath2  32954  lneq2at  32995  llnexchb2  33086  dalawlem1  33088  lhpexle3lem  33228  cdleme26ee  33577  cdlemg34  33929  cdlemg35  33930  cdlemg36  33931  cdlemj1  34038  cdlemj2  34039  cdlemk23-3  34119  cdlemk25-3  34121  cdlemk26b-3  34122  cdlemk26-3  34123  cdleml3N  34195
  Copyright terms: Public domain W3C validator