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

Theorem simpl1l 1286
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 774 . 2 (((𝜑𝜓) ∧ 𝜏) → 𝜑)
213ad2antl1 1229 1 ((((𝜑𝜓) ∧ 𝜒𝜃) ∧ 𝜏) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  soisores  6799  tfisi  7286  omopth2  7899  swrdsbslen  13670  swrdspsleq  13671  repswswrd  13753  ramub1lem1  15945  cntzsubr  19014  lbspss  19287  maducoeval2  20655  cramer  20708  neiptopnei  21148  ptbasin  21592  basqtop  21726  tmdgsum  22110  ustuqtop1  22256  cxplea  24654  cxple2  24655  ewlkle  26727  uspgr2wlkeq2  26769  br8d  29745  isarchi2  30062  archiabllem2c  30072  cvmlift2lem10  31615  nosupbnd2lem1  32180  5segofs  32432  2llnjaN  35344  lvolnle3at  35360  paddasslem12  35609  paddasslem13  35610  atmod1i1m  35636  lhp2lt  35779  lhpexle2lem  35787  lhpmcvr3  35803  lhpat3  35824  ltrneq2  35926  trlnle  35965  trlval3  35966  trlval4  35967  cdleme0moN  36004  cdleme17b  36066  cdlemefrs29pre00  36174  cdlemefr27cl  36182  cdleme42ke  36264  cdleme42mgN  36267  cdleme46f2g2  36272  cdleme46f2g1  36273  cdleme50eq  36320  cdleme50trn3  36332  trlord  36348  cdlemg6c  36399  cdlemg11b  36421  cdlemg18a  36457  cdlemg42  36508  cdlemg46  36514  trljco  36519  tendococl  36551  cdlemj3  36602  tendotr  36609  cdlemk35s-id  36717  cdlemk39s-id  36719  cdlemk53b  36735  cdlemk53  36736  cdlemk35u  36743  tendoex  36754  cdlemm10N  36897  dihopelvalcpre  37027  dihord6apre  37035  dihord5b  37038  dihglblem5apreN  37070  dihglblem2N  37073  dihmeetlem4preN  37085  dihmeetlem6  37088  dihmeetlem10N  37095  dihmeetlem11N  37096  dihmeetlem16N  37101  dihmeetlem17N  37102  dihmeetlem18N  37103  dihmeetlem19N  37104  dihmeetALTN  37106  dihlspsnat  37112  dvh3dim2  37227  dvh3dim3N  37228  jm2.25lem1  38064  jm2.26  38068  limcperiod  40338  0ellimcdiv  40359  cncfshift  40565  cncfperiod  40570  icccncfext  40578  stoweidlem34  40728  fourierdlem48  40848  fourierdlem87  40887  sge0xaddlem2  41128  smflimsuplem7  41512  domnmsuppn0  42716
  Copyright terms: Public domain W3C validator