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

Theorem simpl1l 1039
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 1012 . 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 965
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 967
This theorem is referenced by:  soisores  6013  tfisi  6464  omopth2  7015  repswswrd  12414  ramub1lem1  14079  cntzsubr  16875  lbspss  17140  maducoeval2  18421  cramer  18472  neiptopnei  18711  ptbasin  19125  basqtop  19259  tmdgsum  19641  ustuqtop1  19791  cxplea  22116  cxple2  22117  br8d  25893  isarchi2  26153  archiabllem2c  26163  cvmlift2lem10  27153  5segofs  27988  jm2.25lem1  29300  jm2.26  29304  stoweidlem34  29782  usg2wlkeq2  30294  domnmsuppn0  30733  2llnjaN  33050  lvolnle3at  33066  paddasslem12  33315  paddasslem13  33316  atmod1i1m  33342  lhp2lt  33485  lhpexle2lem  33493  lhpmcvr3  33509  lhpat3  33530  ltrneq2  33632  trlnle  33670  trlval3  33671  trlval4  33672  cdleme0moN  33709  cdleme17b  33771  cdlemefrs29pre00  33879  cdlemefr27cl  33887  cdleme42ke  33969  cdleme42mgN  33972  cdleme46f2g2  33977  cdleme46f2g1  33978  cdleme50eq  34025  cdleme50trn3  34037  trlord  34053  cdlemg6c  34104  cdlemg11b  34126  cdlemg18a  34162  cdlemg42  34213  cdlemg46  34219  trljco  34224  tendococl  34256  cdlemj3  34307  tendotr  34314  cdlemk35s-id  34422  cdlemk39s-id  34424  cdlemk53b  34440  cdlemk53  34441  cdlemk35u  34448  tendoex  34459  cdlemm10N  34603  dihopelvalcpre  34733  dihord6apre  34741  dihord5b  34744  dihglblem5apreN  34776  dihglblem2N  34779  dihmeetlem4preN  34791  dihmeetlem6  34794  dihmeetlem10N  34801  dihmeetlem11N  34802  dihmeetlem16N  34807  dihmeetlem17N  34808  dihmeetlem18N  34809  dihmeetlem19N  34810  dihmeetALTN  34812  dihlspsnat  34818  dvh3dim2  34933  dvh3dim3N  34934
  Copyright terms: Public domain W3C validator