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

Theorem simpl1l 1132
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simpl1l ((((𝜑𝜓) ∧ 𝜒𝜃) ∧ 𝜏) → 𝜑)

Proof of Theorem simpl1l
StepHypRef Expression
1 simp1l 1105 . 2 (((𝜑𝜓) ∧ 𝜒𝜃) → 𝜑)
21adantr 480 1 ((((𝜑𝜓) ∧ 𝜒𝜃) ∧ 𝜏) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054
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 197  df-an 385  df-3an 1056
This theorem is referenced by:  soisores  6617  tfisi  7100  omopth2  7709  swrdsbslen  13494  swrdspsleq  13495  repswswrd  13577  ramub1lem1  15777  cntzsubr  18860  lbspss  19130  maducoeval2  20494  cramer  20545  neiptopnei  20984  ptbasin  21428  basqtop  21562  tmdgsum  21946  ustuqtop1  22092  cxplea  24487  cxple2  24488  ewlkle  26557  uspgr2wlkeq2  26599  br8d  29548  isarchi2  29867  archiabllem2c  29877  cvmlift2lem10  31420  nosupbnd2lem1  31986  5segofs  32238  2llnjaN  35170  lvolnle3at  35186  paddasslem12  35435  paddasslem13  35436  atmod1i1m  35462  lhp2lt  35605  lhpexle2lem  35613  lhpmcvr3  35629  lhpat3  35650  ltrneq2  35752  trlnle  35791  trlval3  35792  trlval4  35793  cdleme0moN  35830  cdleme17b  35892  cdlemefrs29pre00  36000  cdlemefr27cl  36008  cdleme42ke  36090  cdleme42mgN  36093  cdleme46f2g2  36098  cdleme46f2g1  36099  cdleme50eq  36146  cdleme50trn3  36158  trlord  36174  cdlemg6c  36225  cdlemg11b  36247  cdlemg18a  36283  cdlemg42  36334  cdlemg46  36340  trljco  36345  tendococl  36377  cdlemj3  36428  tendotr  36435  cdlemk35s-id  36543  cdlemk39s-id  36545  cdlemk53b  36561  cdlemk53  36562  cdlemk35u  36569  tendoex  36580  cdlemm10N  36724  dihopelvalcpre  36854  dihord6apre  36862  dihord5b  36865  dihglblem5apreN  36897  dihglblem2N  36900  dihmeetlem4preN  36912  dihmeetlem6  36915  dihmeetlem10N  36922  dihmeetlem11N  36923  dihmeetlem16N  36928  dihmeetlem17N  36929  dihmeetlem18N  36930  dihmeetlem19N  36931  dihmeetALTN  36933  dihlspsnat  36939  dvh3dim2  37054  dvh3dim3N  37055  jm2.25lem1  37882  jm2.26  37886  limcperiod  40178  0ellimcdiv  40199  cncfshift  40405  cncfperiod  40410  icccncfext  40418  stoweidlem34  40569  fourierdlem48  40689  fourierdlem87  40728  sge0xaddlem2  40969  smflimsuplem7  41353  domnmsuppn0  42475
  Copyright terms: Public domain W3C validator