Theorem simpll1 1212

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 724	1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1087

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 397  df-3an 1089

This theorem is referenced by:  f1prex  7281  poxp3  8135  ordiso2  9509  hartogslem1  9536  wemapso2lem  9546  acndom  10045  fin1a2lem12  10405  fin1a2lem13  10406  prlem934  11027  ifle  13175  lcmfunsnlem2lem1  16574  divgcdcoprm0  16601  rpexp  16658  qexpz  16833  ramval  16940  0ram  16952  ramz2  16956  initoeu2lem2  17964  mrelatglb  18512  dfgrp3lem  18920  odbezout  19425  rhmdvdsr  20286  lsmcl  20693  lbsextlem3  20772  frlmsslsp  21350  islindf4  21392  psropprmul  21759  coe1mul2  21790  coe1fzgsumdlem  21824  evl1gsumdlem  21874  scmate  22011  mdetunilem7  22119  mdetmul  22124  cramerlem2  22189  m2pmfzgsumcl  22249  decpmatmul  22273  pmatcollpw3lem  22284  chpdmatlem2  22340  cpmadugsumlemB  22375  cpmadugsumlemC  22376  cpmadugsumlemF  22377  chcoeffeqlem  22386  cnconst2  22786  ordthauslem  22886  clsconn  22933  restnlly  22985  comppfsc  23035  ptpjopn  23115  trfg  23394  rnelfmlem  23455  isfcf  23537  fcfnei  23538  cnpfcf  23544  utop2nei  23754  neipcfilu  23800  blssps  23929  blss  23930  metcnp  24049  xrsxmet  24324  metdsge  24364  metdseq0  24369  addcnlem  24379  xrhmeo  24461  nmhmcn  24635  caucfil  24799  limcfval  25388  fta1b  25686  lgsmod  26823  lgsdir  26832  lgsne0  26835  nosupbnd1lem3  27210  nosupbnd1lem4  27211  nosupbnd1lem5  27212  nosupbnd2  27216  noinfbnd1lem3  27225  noinfbnd1lem4  27226  noinfbnd1lem5  27227  noinfbnd2  27231  scutun12  27308  sltlpss  27398  sleadd1  27469  axpasch  28196  axcontlem2  28220  clwwlknonex2  29359  frgr3v  29525  pjhthmo  30550  difioo  31988  xrge0adddir  32188  archiabl  32339  ssmxidl  32585  dimvalfi  32682  probun  33413  satfv1lem  34348  trisegint  34995  btwnconn1lem13  35066  brsegle2  35076  linethru  35120  lindsadd  36476  hlrelat  38268  intnatN  38273  lnnat  38293  3dim0  38323  3dim1  38333  3dim2  38334  atcvrlln  38386  llnexatN  38387  2at0mat0  38391  llncvrlpln  38424  lplnexllnN  38430  lplncvrlvol  38482  lncvrelatN  38647  lncmp  38649  elpaddn0  38666  paddasslem5  38690  pmapjoin  38718  pmapjat1  38719  pclclN  38757  osumclN  38833  lhprelat3N  38906  trlval4  39054  cdlemd5  39068  cdleme32fvcl  39306  cdleme42keg  39352  cdlemg1a  39436  cdlemg1cN  39453  cdlemg39  39582  ltrncom  39604  cdlemk34  39776  dihord2pre  40091  dihopelvalcpre  40114  dihmeetALTN  40193  dihlspsnssN  40198  dihlspsnat  40199  diophrw  41487  lzunuz  41496  qirropth  41636  jm2.19  41722  jm2.27  41737  lmhmfgsplit  41818  hbtlem5  41860  nadd2rabtr  42124  naddsuc2  42133  fzunt  42196  iunrelexpuztr  42460  rfcnnnub  43710  3adantll2  43715  3adantll3  43716  ioondisj2  44196  ioondisj1  44197  iccintsng  44226  icccncfext  44593  stoweidlem20  44726  stoweidlem61  44767  smflimlem2  45478  rnglidlmcl  46738  rmsupp0  47034  rmsuppss  47036  ply1mulgsum  47061  rrxlinesc  47411