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

Theorem simpl1l 1056
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 1029 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ph )
21adantr 466 1  |-  ( ( ( ( ph  /\  ps )  /\  ch  /\  th )  /\  ta )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  soisores  6230  tfisi  6696  omopth2  7290  swrdsbslen  12795  swrdspsleq  12796  repswswrd  12878  ramub1lem1  14972  cntzsubr  18028  lbspss  18293  maducoeval2  19652  cramer  19703  neiptopnei  20135  ptbasin  20579  basqtop  20713  tmdgsum  21097  ustuqtop1  21243  cxplea  23628  cxple2  23629  usg2wlkeq2  25423  br8d  28208  isarchi2  28497  archiabllem2c  28507  cvmlift2lem10  30031  5segofs  30766  2llnjaN  33050  lvolnle3at  33066  paddasslem12  33315  paddasslem13  33316  atmod1i1m  33342  lhp2lt  33485  lhpexle2lem  33493  lhpmcvr3  33509  lhpat3  33530  ltrneq2  33632  trlnle  33671  trlval3  33672  trlval4  33673  cdleme0moN  33710  cdleme17b  33772  cdlemefrs29pre00  33881  cdlemefr27cl  33889  cdleme42ke  33971  cdleme42mgN  33974  cdleme46f2g2  33979  cdleme46f2g1  33980  cdleme50eq  34027  cdleme50trn3  34039  trlord  34055  cdlemg6c  34106  cdlemg11b  34128  cdlemg18a  34164  cdlemg42  34215  cdlemg46  34221  trljco  34226  tendococl  34258  cdlemj3  34309  tendotr  34316  cdlemk35s-id  34424  cdlemk39s-id  34426  cdlemk53b  34442  cdlemk53  34443  cdlemk35u  34450  tendoex  34461  cdlemm10N  34605  dihopelvalcpre  34735  dihord6apre  34743  dihord5b  34746  dihglblem5apreN  34778  dihglblem2N  34781  dihmeetlem4preN  34793  dihmeetlem6  34796  dihmeetlem10N  34803  dihmeetlem11N  34804  dihmeetlem16N  34809  dihmeetlem17N  34810  dihmeetlem18N  34811  dihmeetlem19N  34812  dihmeetALTN  34814  dihlspsnat  34820  dvh3dim2  34935  dvh3dim3N  34936  jm2.25lem1  35773  jm2.26  35777  limcperiod  37528  0ellimcdiv  37550  cncfshift  37571  cncfperiod  37576  icccncfext  37585  stoweidlem34  37715  fourierdlem48  37838  fourierdlem87  37877  sge0xaddlem2  38064  domnmsuppn0  39428
  Copyright terms: Public domain W3C validator