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

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

Proof of Theorem simpl1l
StepHypRef Expression
1 simp1l 1020 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ph )
21adantr 465 1  |-  ( ( ( ( ph  /\  ps )  /\  ch  /\  th )  /\  ta )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973
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 371  df-3an 975
This theorem is referenced by:  soisores  6209  tfisi  6671  omopth2  7230  repswswrd  12715  ramub1lem1  14399  cntzsubr  17244  lbspss  17511  maducoeval2  18909  cramer  18960  neiptopnei  19399  ptbasin  19813  basqtop  19947  tmdgsum  20329  ustuqtop1  20479  cxplea  22805  cxple2  22806  usg2wlkeq2  24385  br8d  27136  isarchi2  27391  archiabllem2c  27401  cvmlift2lem10  28397  5segofs  29233  jm2.25lem1  30544  jm2.26  30548  limcperiod  31170  0ellimcdiv  31191  cncfshift  31212  cncfperiod  31217  icccncfext  31226  stoweidlem34  31334  fourierdlem48  31455  fourierdlem87  31494  domnmsuppn0  32035  2llnjaN  34362  lvolnle3at  34378  paddasslem12  34627  paddasslem13  34628  atmod1i1m  34654  lhp2lt  34797  lhpexle2lem  34805  lhpmcvr3  34821  lhpat3  34842  ltrneq2  34944  trlnle  34982  trlval3  34983  trlval4  34984  cdleme0moN  35021  cdleme17b  35083  cdlemefrs29pre00  35191  cdlemefr27cl  35199  cdleme42ke  35281  cdleme42mgN  35284  cdleme46f2g2  35289  cdleme46f2g1  35290  cdleme50eq  35337  cdleme50trn3  35349  trlord  35365  cdlemg6c  35416  cdlemg11b  35438  cdlemg18a  35474  cdlemg42  35525  cdlemg46  35531  trljco  35536  tendococl  35568  cdlemj3  35619  tendotr  35626  cdlemk35s-id  35734  cdlemk39s-id  35736  cdlemk53b  35752  cdlemk53  35753  cdlemk35u  35760  tendoex  35771  cdlemm10N  35915  dihopelvalcpre  36045  dihord6apre  36053  dihord5b  36056  dihglblem5apreN  36088  dihglblem2N  36091  dihmeetlem4preN  36103  dihmeetlem6  36106  dihmeetlem10N  36113  dihmeetlem11N  36114  dihmeetlem16N  36119  dihmeetlem17N  36120  dihmeetlem18N  36121  dihmeetlem19N  36122  dihmeetALTN  36124  dihlspsnat  36130  dvh3dim2  36245  dvh3dim3N  36246
  Copyright terms: Public domain W3C validator