Theorem simpll1 1213

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)

Assertion

Ref	Expression
simpll1	⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)

Proof of Theorem simpll1

Step	Hyp	Ref	Expression
1		simp1 1136	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
2	1	ad2antrr 726	1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  f1prex  7225  poxp3  8090  naddsuc2  8626  ordiso2  9426  hartogslem1  9453  wemapso2lem  9463  acndom  9964  fin1a2lem12  10324  fin1a2lem13  10325  prlem934  10946  ifle  13117  lcmfunsnlem2lem1  16567  divgcdcoprm0  16594  rpexp  16651  qexpz  16831  ramval  16938  0ram  16950  ramz2  16954  initoeu2lem2  17940  mrelatglb  18484  dfgrp3lem  18935  odbezout  19455  rhmdvdsr  20411  lsmcl  21005  lbsextlem3  21085  rnglidlmcl  21141  frlmsslsp  21721  islindf4  21763  psropprmul  22138  coe1mul2  22171  coe1fzgsumdlem  22206  evl1gsumdlem  22259  scmate  22413  mdetunilem7  22521  mdetmul  22526  cramerlem2  22591  m2pmfzgsumcl  22651  decpmatmul  22675  pmatcollpw3lem  22686  chpdmatlem2  22742  cpmadugsumlemB  22777  cpmadugsumlemC  22778  cpmadugsumlemF  22779  chcoeffeqlem  22788  cnconst2  23186  ordthauslem  23286  clsconn  23333  restnlly  23385  comppfsc  23435  ptpjopn  23515  trfg  23794  rnelfmlem  23855  isfcf  23937  fcfnei  23938  cnpfcf  23944  utop2nei  24154  neipcfilu  24199  blssps  24328  blss  24329  metcnp  24445  xrsxmet  24714  metdsge  24754  metdseq0  24759  addcnlem  24769  xrhmeo  24860  nmhmcn  25036  caucfil  25199  limcfval  25789  fta1b  26093  lgsmod  27250  lgsdir  27259  lgsne0  27262  nosupbnd1lem3  27638  nosupbnd1lem4  27639  nosupbnd1lem5  27640  nosupbnd2  27644  noinfbnd1lem3  27653  noinfbnd1lem4  27654  noinfbnd1lem5  27655  noinfbnd2  27659  scutun12  27739  sltlpss  27840  sleadd1  27919  axpasch  28904  axcontlem2  28928  clwwlknonex2  30071  frgr3v  30237  pjhthmo  31264  difioo  32738  xrge0adddir  32985  archiabl  33153  ssmxidl  33424  dimvalfi  33576  probun  34389  satfv1lem  35337  trisegint  36004  btwnconn1lem13  36075  brsegle2  36085  linethru  36129  lindsadd  37595  hlrelat  39384  intnatN  39389  lnnat  39409  3dim0  39439  3dim1  39449  3dim2  39450  atcvrlln  39502  llnexatN  39503  2at0mat0  39507  llncvrlpln  39540  lplnexllnN  39546  lplncvrlvol  39598  lncvrelatN  39763  lncmp  39765  elpaddn0  39782  paddasslem5  39806  pmapjoin  39834  pmapjat1  39835  pclclN  39873  osumclN  39949  lhprelat3N  40022  trlval4  40170  cdlemd5  40184  cdleme32fvcl  40422  cdleme42keg  40468  cdlemg1a  40552  cdlemg1cN  40569  cdlemg39  40698  ltrncom  40720  cdlemk34  40892  dihord2pre  41207  dihopelvalcpre  41230  dihmeetALTN  41309  dihlspsnssN  41314  dihlspsnat  41315  aks6d1c6isolem1  42150  diophrw  42735  lzunuz  42744  qirropth  42884  jm2.19  42969  jm2.27  42984  lmhmfgsplit  43062  hbtlem5  43104  nadd2rabtr  43360  fzunt  43431  iunrelexpuztr  43695  rfcnnnub  45017  3adantll2  45022  3adantll3  45023  ioondisj2  45478  ioondisj1  45479  iccintsng  45508  icccncfext  45872  stoweidlem20  46005  stoweidlem61  46046  smflimlem2  46757  isuspgrim0lem  47881  isuspgrim0  47882  rmsupp0  48356  rmsuppss  48358  ply1mulgsum  48379  rrxlinesc  48724