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

Theorem simp122 1121
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 1022 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )  /\  ta )  ->  ps )
213ad2ant1 1009 1  |-  ( ( ( th  /\  ( ph  /\  ps  /\  ch )  /\  ta )  /\  et  /\  ze )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 965
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 967
This theorem is referenced by:  ax5seglem3  23356  axpasch  23366  exatleN  33411  ps-2b  33489  3atlem1  33490  3atlem2  33491  3atlem4  33493  3atlem5  33494  3atlem6  33495  2llnjaN  33573  4atlem12b  33618  2lplnja  33626  dalemqea  33634  dath2  33744  lneq2at  33785  llnexchb2  33876  dalawlem1  33878  lhpexle3lem  34018  cdleme26ee  34367  cdlemg34  34719  cdlemg35  34720  cdlemg36  34721  cdlemj1  34828  cdlemj2  34829  cdlemk23-3  34909  cdlemk25-3  34911  cdlemk26b-3  34912  cdlemk26-3  34913  cdleml3N  34985
  Copyright terms: Public domain W3C validator