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

Theorem simpl11 1069
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 1024 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th  /\  ta )  ->  ph )
21adantr 463 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th 
/\  ta )  /\  et )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 971
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 369  df-3an 973
This theorem is referenced by:  pythagtriplem4  14430  tsmsxp  20826  brbtwn2  24413  ax5seg  24446  br8  29429  btwndiff  29908  ifscgr  29925  seglecgr12im  29991  fourierdlem77  32208  lkrshp  35246  cvlcvr1  35480  atbtwn  35586  3dimlem3  35601  3dimlem3OLDN  35602  1cvratex  35613  llnmlplnN  35679  4atlem3  35736  4atlem3a  35737  4atlem11  35749  4atlem12  35752  lnatexN  35919  cdlemb  35934  paddasslem4  35963  paddasslem10  35969  pmodlem1  35986  llnexchb2lem  36008  llnexchb2  36009  arglem1N  36331  cdlemd4  36342  cdlemd9  36347  cdlemd  36348  cdleme16  36426  cdleme20  36466  cdleme21i  36477  cdleme21k  36480  cdleme27N  36511  cdleme28c  36514  cdlemefrs29bpre0  36538  cdlemefrs29clN  36541  cdlemefrs32fva  36542  cdleme41sn3a  36575  cdleme32fva  36579  cdleme40n  36610  cdlemg12e  36789  cdlemg15a  36797  cdlemg15  36798  cdlemg16ALTN  36800  cdlemg16z  36801  cdlemg20  36827  cdlemg22  36829  cdlemg29  36847  cdlemg38  36857  cdlemk33N  37051  cdlemk56  37113  dihord11b  37365  dihord2pre  37368  dihord4  37401
  Copyright terms: Public domain W3C validator