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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  f1prex  7293  poxp3  8155  naddsuc2  8697  ordiso2  9487  hartogslem1  9514  wemapso2lem  9524  acndom  10054  fin1a2lem12  10413  fin1a2lem13  10414  prlem934  11036  ifle  13241  lcmfunsnlem2lem1  16721  divgcdcoprm0  16748  rpexp  16806  qexpz  16986  ramval  17093  0ram  17105  ramz2  17109  initoeu2lem2  18097  mrelatglb  18641  dfgrp3lem  19135  odbezout  19659  rhmdvdsr  20642  lsmcl  21241  lbsextlem3  21321  rnglidlmcl  21378  frlmsslsp  21983  islindf4  22025  psropprmul  22434  coe1mul2  22467  coe1fzgsumdlem  22500  evl1gsumdlem  22553  scmate  22704  mdetunilem7  22812  mdetmul  22817  cramerlem2  22882  m2pmfzgsumcl  22942  decpmatmul  22966  pmatcollpw3lem  22977  chpdmatlem2  23033  cpmadugsumlemB  23068  cpmadugsumlemC  23069  cpmadugsumlemF  23070  chcoeffeqlem  23079  cnconst2  23477  ordthauslem  23577  clsconn  23624  restnlly  23676  comppfsc  23726  ptpjopn  23806  trfg  24085  rnelfmlem  24146  isfcf  24228  fcfnei  24229  cnpfcf  24235  utop2nei  24444  neipcfilu  24489  blssps  24618  blss  24619  metcnp  24735  xrsxmet  25004  metdsge  25044  metdseq0  25049  addcnlem  25059  xrhmeo  25142  nmhmcn  25316  caucfil  25479  limcfval  26068  fta1b  26366  lgsmod  27524  lgsdir  27533  lgsne0  27536  nosupbnd1lem3  27911  nosupbnd1lem4  27912  nosupbnd1lem5  27913  nosupbnd2  27917  noinfbnd1lem3  27926  noinfbnd1lem4  27927  noinfbnd1lem5  27928  noinfbnd2  27932  cutsun12  28020  ltslpss  28138  leadds1  28219  axpasch  29328  axcontlem2  29352  clwwlknonex2  30497  frgr3v  30663  pjhthmo  31691  difioo  33164  xrge0adddir  33369  archiabl  33549  ssmxidl  33788  dimvalfi  34023  probun  34841  satfv1lem  35875  trisegint  36541  btwnconn1lem13  36612  brsegle2  36622  linethru  36666  lindsadd  38305  hlrelat  40217  intnatN  40222  lnnat  40242  3dim0  40272  3dim1  40282  3dim2  40283  atcvrlln  40335  llnexatN  40336  2at0mat0  40340  llncvrlpln  40373  lplnexllnN  40379  lplncvrlvol  40431  lncvrelatN  40596  lncmp  40598  elpaddn0  40615  paddasslem5  40639  pmapjoin  40667  pmapjat1  40668  pclclN  40706  osumclN  40782  lhprelat3N  40855  trlval4  41003  cdlemd5  41017  cdleme32fvcl  41255  cdleme42keg  41301  cdlemg1a  41385  cdlemg1cN  41402  cdlemg39  41531  ltrncom  41553  cdlemk34  41725  dihord2pre  42040  dihopelvalcpre  42063  dihmeetALTN  42142  dihlspsnssN  42147  dihlspsnat  42148  aks6d1c6isolem1  42982  diophrw  43531  lzunuz  43540  qirropth  43676  jm2.19  43761  jm2.27  43776  lmhmfgsplit  43854  hbtlem5  43896  nadd2rabtr  44152  fzunt  44222  iunrelexpuztr  44486  rfcnnnub  45797  3adantll2  45802  3adantll3  45803  ioondisj2  46250  ioondisj1  46251  iccintsng  46280  icccncfext  46642  stoweidlem20  46775  stoweidlem61  46816  smflimlem2  47527  isuspgrim0lem  48699  isuspgrim0  48700  rmsupp0  49189  rmsuppss  49191  ply1mulgsum  49211  rrxlinesc  49556