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

Theorem simpl11 1030
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 985 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th  /\  ta )  ->  ph )
21adantr 451 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th 
/\  ta )  /\  et )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  pythagtriplem4  12872  tsmsxp  17837  br8  24113  brbtwn2  24533  ax5seg  24566  btwndiff  24650  ifscgr  24667  seglecgr12im  24733  lkrshp  29295  cvlcvr1  29529  atbtwn  29635  3dimlem3  29650  3dimlem3OLDN  29651  1cvratex  29662  llnmlplnN  29728  4atlem3  29785  4atlem3a  29786  4atlem11  29798  4atlem12  29801  lnatexN  29968  cdlemb  29983  paddasslem4  30012  paddasslem10  30018  pmodlem1  30035  llnexchb2lem  30057  llnexchb2  30058  arglem1N  30379  cdlemd4  30390  cdlemd9  30395  cdlemd  30396  cdleme16  30474  cdleme20  30513  cdleme21i  30524  cdleme21k  30527  cdleme27N  30558  cdleme28c  30561  cdlemefrs29bpre0  30585  cdlemefrs29clN  30588  cdlemefrs32fva  30589  cdleme41sn3a  30622  cdleme32fva  30626  cdleme40n  30657  cdlemg12e  30836  cdlemg15a  30844  cdlemg15  30845  cdlemg16ALTN  30847  cdlemg16z  30848  cdlemg20  30874  cdlemg22  30876  cdlemg29  30894  cdlemg38  30904  cdlemk33N  31098  cdlemk56  31160  dihord11b  31412  dihord2pre  31415  dihord4  31448
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