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

Theorem simpl1l 1218
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 763 . 2 (((𝜑𝜓) ∧ 𝜏) → 𝜑)
213ad2antl1 1179 1 ((((𝜑𝜓) ∧ 𝜒𝜃) ∧ 𝜏) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1081
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 208  df-an 397  df-3an 1083
This theorem is referenced by:  soisores  7072  tfisi  7561  funelss  7737  omopth2  8200  swrdsbslen  14016  swrdspsleq  14017  repswswrd  14136  ramub1lem1  16352  cntzsubr  19488  lbspss  19774  maducoeval2  21165  cramer  21216  neiptopnei  21656  ptbasin  22101  basqtop  22235  tmdgsum  22619  ustuqtop1  22765  cxplea  25192  cxple2  25193  ewlkle  27301  uspgr2wlkeq2  27342  clwwlkccat  27682  br8d  30276  isarchi2  30728  archiabllem2c  30738  cvmlift2lem10  32443  nosupbnd2lem1  33099  5segofs  33351  2llnjaN  36569  lvolnle3at  36585  paddasslem12  36834  paddasslem13  36835  atmod1i1m  36861  lhp2lt  37004  lhpexle2lem  37012  lhpmcvr3  37028  lhpat3  37049  ltrneq2  37151  trlnle  37189  trlval3  37190  trlval4  37191  cdleme0moN  37228  cdleme17b  37290  cdlemefrs29pre00  37398  cdlemefr27cl  37406  cdleme42ke  37488  cdleme42mgN  37491  cdleme46f2g2  37496  cdleme46f2g1  37497  cdleme50eq  37544  cdleme50trn3  37556  trlord  37572  cdlemg6c  37623  cdlemg11b  37645  cdlemg18a  37681  cdlemg42  37732  cdlemg46  37738  trljco  37743  tendococl  37775  cdlemj3  37826  tendotr  37833  cdlemk35s-id  37941  cdlemk39s-id  37943  cdlemk53b  37959  cdlemk53  37960  cdlemk35u  37967  tendoex  37978  cdlemm10N  38121  dihopelvalcpre  38251  dihord6apre  38259  dihord5b  38262  dihglblem5apreN  38294  dihglblem2N  38297  dihmeetlem4preN  38309  dihmeetlem6  38312  dihmeetlem10N  38319  dihmeetlem11N  38320  dihmeetlem16N  38325  dihmeetlem17N  38326  dihmeetlem18N  38327  dihmeetlem19N  38328  dihmeetALTN  38330  dihlspsnat  38336  dvh3dim2  38451  dvh3dim3N  38452  jm2.25lem1  39460  jm2.26  39464  grur1cld  40433  limcperiod  41774  0ellimcdiv  41795  cncfshift  42022  cncfperiod  42027  icccncfext  42035  stoweidlem34  42185  fourierdlem48  42305  fourierdlem87  42344  sge0xaddlem2  42582  smflimsuplem7  42966  isomgrsym  43833  domnmsuppn0  44249  itscnhlinecirc02plem2  44602
  Copyright terms: Public domain W3C validator