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

Theorem simpl1l 1225
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)
Assertion
Ref Expression
simpl1l ((((𝜑𝜓) ∧ 𝜒𝜃) ∧ 𝜏) → 𝜑)

Proof of Theorem simpl1l
StepHypRef Expression
1 simpll 766 . 2 (((𝜑𝜓) ∧ 𝜏) → 𝜑)
213ad2antl1 1186 1 ((((𝜑𝜓) ∧ 𝜒𝜃) ∧ 𝜏) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088
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 206  df-an 398  df-3an 1090
This theorem is referenced by:  soisores  7273  tfisi  7796  funelss  7980  omopth2  8532  swrdsbslen  14558  swrdspsleq  14559  repswswrd  14678  ramub1lem1  16903  cntzsubr  20269  lbspss  20558  maducoeval2  22005  cramer  22056  neiptopnei  22499  ptbasin  22944  basqtop  23078  tmdgsum  23462  ustuqtop1  23609  cxplea  26067  cxple2  26068  nosupbnd2lem1  27079  noinfbnd2lem1  27094  ewlkle  28595  uspgr2wlkeq2  28637  clwwlkccat  28976  br8d  31575  isarchi2  32070  archiabllem2c  32080  cvmlift2lem10  33963  5segofs  34637  2llnjaN  38075  lvolnle3at  38091  paddasslem12  38340  paddasslem13  38341  atmod1i1m  38367  lhp2lt  38510  lhpexle2lem  38518  lhpmcvr3  38534  lhpat3  38555  ltrneq2  38657  trlnle  38695  trlval3  38696  trlval4  38697  cdleme0moN  38734  cdleme17b  38796  cdlemefrs29pre00  38904  cdlemefr27cl  38912  cdleme42ke  38994  cdleme42mgN  38997  cdleme46f2g2  39002  cdleme46f2g1  39003  cdleme50eq  39050  cdleme50trn3  39062  trlord  39078  cdlemg6c  39129  cdlemg11b  39151  cdlemg18a  39187  cdlemg42  39238  cdlemg46  39244  trljco  39249  tendococl  39281  cdlemj3  39332  tendotr  39339  cdlemk35s-id  39447  cdlemk39s-id  39449  cdlemk53b  39465  cdlemk53  39466  cdlemk35u  39473  tendoex  39484  cdlemm10N  39627  dihopelvalcpre  39757  dihord6apre  39765  dihord5b  39768  dihglblem5apreN  39800  dihglblem2N  39803  dihmeetlem4preN  39815  dihmeetlem6  39818  dihmeetlem10N  39825  dihmeetlem11N  39826  dihmeetlem16N  39831  dihmeetlem17N  39832  dihmeetlem18N  39833  dihmeetlem19N  39834  dihmeetALTN  39836  dihlspsnat  39842  dvh3dim2  39957  dvh3dim3N  39958  jm2.25lem1  41365  jm2.26  41369  grur1cld  42600  limcperiod  43955  0ellimcdiv  43976  cncfshift  44201  cncfperiod  44206  icccncfext  44214  stoweidlem34  44361  fourierdlem48  44481  fourierdlem87  44520  sge0xaddlem2  44761  smflimsuplem7  45153  isomgrsym  46114  domnmsuppn0  46531  itscnhlinecirc02plem2  46955
  Copyright terms: Public domain W3C validator