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

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

Proof of Theorem simpl11
StepHypRef Expression
1 simp11 988 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th  /\  ta )  ->  ph )
21adantr 453 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th 
/\  ta )  /\  et )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  pythagtriplem4  13195  tsmsxp  18186  br8  25381  brbtwn2  25846  ax5seg  25879  btwndiff  25963  ifscgr  25980  seglecgr12im  26046  lkrshp  29965  cvlcvr1  30199  atbtwn  30305  3dimlem3  30320  3dimlem3OLDN  30321  1cvratex  30332  llnmlplnN  30398  4atlem3  30455  4atlem3a  30456  4atlem11  30468  4atlem12  30471  lnatexN  30638  cdlemb  30653  paddasslem4  30682  paddasslem10  30688  pmodlem1  30705  llnexchb2lem  30727  llnexchb2  30728  arglem1N  31049  cdlemd4  31060  cdlemd9  31065  cdlemd  31066  cdleme16  31144  cdleme20  31183  cdleme21i  31194  cdleme21k  31197  cdleme27N  31228  cdleme28c  31231  cdlemefrs29bpre0  31255  cdlemefrs29clN  31258  cdlemefrs32fva  31259  cdleme41sn3a  31292  cdleme32fva  31296  cdleme40n  31327  cdlemg12e  31506  cdlemg15a  31514  cdlemg15  31515  cdlemg16ALTN  31517  cdlemg16z  31518  cdlemg20  31544  cdlemg22  31546  cdlemg29  31564  cdlemg38  31574  cdlemk33N  31768  cdlemk56  31830  dihord11b  32082  dihord2pre  32085  dihord4  32118
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator