Theorem simpll1 1231

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 1154	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
2	1	ad2antrr 738	1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  f1prex  7284  poxp3  8147  naddsuc2  8689  ordiso2  9478  hartogslem1  9505  wemapso2lem  9515  acndom  10036  fin1a2lem12  10396  fin1a2lem13  10397  prlem934  11019  ifle  13224  lcmfunsnlem2lem1  16697  divgcdcoprm0  16724  rpexp  16782  qexpz  16962  ramval  17069  0ram  17081  ramz2  17085  initoeu2lem2  18073  mrelatglb  18617  dfgrp3lem  19105  odbezout  19629  rhmdvdsr  20592  lsmcl  21185  lbsextlem3  21265  rnglidlmcl  21322  frlmsslsp  21927  islindf4  21969  psropprmul  22378  coe1mul2  22411  coe1fzgsumdlem  22444  evl1gsumdlem  22497  scmate  22648  mdetunilem7  22756  mdetmul  22761  cramerlem2  22826  m2pmfzgsumcl  22886  decpmatmul  22910  pmatcollpw3lem  22921  chpdmatlem2  22977  cpmadugsumlemB  23012  cpmadugsumlemC  23013  cpmadugsumlemF  23014  chcoeffeqlem  23023  cnconst2  23421  ordthauslem  23521  clsconn  23568  restnlly  23620  comppfsc  23670  ptpjopn  23750  trfg  24029  rnelfmlem  24090  isfcf  24172  fcfnei  24173  cnpfcf  24179  utop2nei  24388  neipcfilu  24433  blssps  24562  blss  24563  metcnp  24679  xrsxmet  24948  metdsge  24988  metdseq0  24993  addcnlem  25003  xrhmeo  25086  nmhmcn  25260  caucfil  25423  limcfval  26012  fta1b  26310  lgsmod  27465  lgsdir  27474  lgsne0  27477  nosupbnd1lem3  27852  nosupbnd1lem4  27853  nosupbnd1lem5  27854  nosupbnd2  27858  noinfbnd1lem3  27867  noinfbnd1lem4  27868  noinfbnd1lem5  27869  noinfbnd2  27873  cutsun12  27961  ltslpss  28079  leadds1  28160  axpasch  29269  axcontlem2  29293  clwwlknonex2  30438  frgr3v  30604  pjhthmo  31632  difioo  33105  xrge0adddir  33316  archiabl  33496  ssmxidl  33735  dimvalfi  33970  probun  34787  satfv1lem  35832  trisegint  36498  btwnconn1lem13  36569  brsegle2  36579  linethru  36623  lindsadd  38242  hlrelat  40154  intnatN  40159  lnnat  40179  3dim0  40209  3dim1  40219  3dim2  40220  atcvrlln  40272  llnexatN  40273  2at0mat0  40277  llncvrlpln  40310  lplnexllnN  40316  lplncvrlvol  40368  lncvrelatN  40533  lncmp  40535  elpaddn0  40552  paddasslem5  40576  pmapjoin  40604  pmapjat1  40605  pclclN  40643  osumclN  40719  lhprelat3N  40792  trlval4  40940  cdlemd5  40954  cdleme32fvcl  41192  cdleme42keg  41238  cdlemg1a  41322  cdlemg1cN  41339  cdlemg39  41468  ltrncom  41490  cdlemk34  41662  dihord2pre  41977  dihopelvalcpre  42000  dihmeetALTN  42079  dihlspsnssN  42084  dihlspsnat  42085  aks6d1c6isolem1  42919  diophrw  43470  lzunuz  43479  qirropth  43615  jm2.19  43700  jm2.27  43715  lmhmfgsplit  43793  hbtlem5  43835  nadd2rabtr  44091  fzunt  44161  iunrelexpuztr  44425  rfcnnnub  45736  3adantll2  45741  3adantll3  45742  ioondisj2  46189  ioondisj1  46190  iccintsng  46219  icccncfext  46581  stoweidlem20  46714  stoweidlem61  46755  smflimlem2  47466  isuspgrim0lem  48635  isuspgrim0  48636  rmsupp0  49125  rmsuppss  49127  ply1mulgsum  49147  rrxlinesc  49492