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

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

Proof of Theorem simpl12
StepHypRef Expression
1 simp12 1040 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th  /\  ta )  ->  ps )
21adantr 467 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th 
/\  ta )  /\  et )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    /\ w3a 986
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 189  df-an 373  df-3an 988
This theorem is referenced by:  pythagtriplem4  14781  pmatcollpw1lem1  19810  pmatcollpw1  19812  mp2pm2mplem2  19843  brbtwn2  24947  ax5seg  24980  br8  30408  ifscgr  30823  seglecgr12im  30889  lkrshp  32683  atlatle  32898  cvlcvr1  32917  atbtwn  33023  3dimlem3  33038  3dimlem3OLDN  33039  1cvratex  33050  llnmlplnN  33116  4atlem3  33173  4atlem3a  33174  4atlem11  33186  4atlem12  33189  cdlemb  33371  paddasslem4  33400  paddasslem10  33406  pmodlem1  33423  llnexchb2lem  33445  arglem1N  33768  cdlemd4  33779  cdlemd  33785  cdleme16  33863  cdleme20  33903  cdleme21k  33917  cdleme22cN  33921  cdleme27N  33948  cdleme28c  33951  cdleme29ex  33953  cdleme32fva  34016  cdleme40n  34047  cdlemg15a  34234  cdlemg15  34235  cdlemg16ALTN  34237  cdlemg16z  34238  cdlemg20  34264  cdlemg22  34266  cdlemg29  34284  cdlemg38  34294  cdlemk33N  34488  cdlemk56  34550  fourierdlem77  38057
  Copyright terms: Public domain W3C validator