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

Theorem simpl12 1031
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 986 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th  /\  ta )  ->  ps )
21adantr 451 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th 
/\  ta )  /\  et )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  pythagtriplem4  12969  br8  24671  brbtwn2  25092  ax5seg  25125  ifscgr  25226  seglecgr12im  25292  lkrshp  29364  atlatle  29579  cvlcvr1  29598  atbtwn  29704  3dimlem3  29719  3dimlem3OLDN  29720  1cvratex  29731  llnmlplnN  29797  4atlem3  29854  4atlem3a  29855  4atlem11  29867  4atlem12  29870  cdlemb  30052  paddasslem4  30081  paddasslem10  30087  pmodlem1  30104  llnexchb2lem  30126  arglem1N  30448  cdlemd4  30459  cdlemd  30465  cdleme16  30543  cdleme20  30582  cdleme21k  30596  cdleme22cN  30600  cdleme27N  30627  cdleme28c  30630  cdleme29ex  30632  cdleme32fva  30695  cdleme40n  30726  cdlemg15a  30913  cdlemg15  30914  cdlemg16ALTN  30916  cdlemg16z  30917  cdlemg20  30943  cdlemg22  30945  cdlemg29  30963  cdlemg38  30973  cdlemk33N  31167  cdlemk56  31229
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