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

Theorem simpl1l 1048
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 1021 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ph )
21adantr 463 1  |-  ( ( ( ( ph  /\  ps )  /\  ch  /\  th )  /\  ta )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 974
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 976
This theorem is referenced by:  soisores  6205  tfisi  6675  omopth2  7269  swrdsbslen  12727  swrdspsleq  12728  repswswrd  12810  ramub1lem1  14751  cntzsubr  17779  lbspss  18046  maducoeval2  19432  cramer  19483  neiptopnei  19924  ptbasin  20368  basqtop  20502  tmdgsum  20884  ustuqtop1  21034  cxplea  23369  cxple2  23370  usg2wlkeq2  25113  br8d  27886  isarchi2  28167  archiabllem2c  28177  cvmlift2lem10  29596  5segofs  30331  2llnjaN  32563  lvolnle3at  32579  paddasslem12  32828  paddasslem13  32829  atmod1i1m  32855  lhp2lt  32998  lhpexle2lem  33006  lhpmcvr3  33022  lhpat3  33043  ltrneq2  33145  trlnle  33184  trlval3  33185  trlval4  33186  cdleme0moN  33223  cdleme17b  33285  cdlemefrs29pre00  33394  cdlemefr27cl  33402  cdleme42ke  33484  cdleme42mgN  33487  cdleme46f2g2  33492  cdleme46f2g1  33493  cdleme50eq  33540  cdleme50trn3  33552  trlord  33568  cdlemg6c  33619  cdlemg11b  33641  cdlemg18a  33677  cdlemg42  33728  cdlemg46  33734  trljco  33739  tendococl  33771  cdlemj3  33822  tendotr  33829  cdlemk35s-id  33937  cdlemk39s-id  33939  cdlemk53b  33955  cdlemk53  33956  cdlemk35u  33963  tendoex  33974  cdlemm10N  34118  dihopelvalcpre  34248  dihord6apre  34256  dihord5b  34259  dihglblem5apreN  34291  dihglblem2N  34294  dihmeetlem4preN  34306  dihmeetlem6  34309  dihmeetlem10N  34316  dihmeetlem11N  34317  dihmeetlem16N  34322  dihmeetlem17N  34323  dihmeetlem18N  34324  dihmeetlem19N  34325  dihmeetALTN  34327  dihlspsnat  34333  dvh3dim2  34448  dvh3dim3N  34449  jm2.25lem1  35282  jm2.26  35286  limcperiod  36983  0ellimcdiv  37004  cncfshift  37025  cncfperiod  37030  icccncfext  37039  stoweidlem34  37165  fourierdlem48  37286  fourierdlem87  37325  domnmsuppn0  38454
  Copyright terms: Public domain W3C validator