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  7284  poxp3  8151  naddsuc2  8695  ordiso2  9493  hartogslem1  9520  wemapso2lem  9530  acndom  10111  fin1a2lem12  10470  fin1a2lem13  10471  prlem934  11099  ifle  13308  lcmfunsnlem2lem1  16793  divgcdcoprm0  16820  rpexp  16878  qexpz  17059  ramval  17166  0ram  17178  ramz2  17182  initoeu2lem2  18170  mrelatglb  18714  dfgrp3lem  19228  odbezout  19752  rhmdvdsr  20738  lsmcl  21338  lbsextlem3  21418  rnglidlmcl  21475  frlmsslsp  22082  islindf4  22124  psropprmul  22535  coe1mul2  22568  coe1fzgsumdlem  22601  evl1gsumdlem  22654  scmate  22805  mdetunilem7  22913  mdetmul  22918  cramerlem2  22986  m2pmfzgsumcl  23046  decpmatmul  23070  pmatcollpw3lem  23081  chpdmatlem2  23137  cpmadugsumlemB  23172  cpmadugsumlemC  23173  cpmadugsumlemF  23174  chcoeffeqlem  23183  cnconst2  23581  ordthauslem  23681  clsconn  23728  restnlly  23781  comppfsc  23831  ptpjopn  23911  trfg  24190  rnelfmlem  24251  isfcf  24333  fcfnei  24334  cnpfcf  24340  utop2nei  24549  neipcfilu  24594  blssps  24723  blss  24724  metcnp  24840  xrsxmet  25109  metdsge  25149  metdseq0  25154  addcnlem  25164  xrhmeo  25247  nmhmcn  25421  caucfil  25584  limcfval  26172  fta1b  26470  lgsmod  27632  lgsdir  27641  lgsne0  27644  nosupbnd1lem3  28049  nosupbnd1lem4  28050  nosupbnd1lem5  28051  nosupbnd2  28055  noinfbnd1lem3  28064  noinfbnd1lem4  28065  noinfbnd1lem5  28066  noinfbnd2  28070  cutsun12  28158  ltslpss  28276  leadds1  28357  axpasch  29501  axcontlem2  29525  clwwlknonex2  30682  frgr3v  30858  pjhthmo  31886  difioo  33356  xrge0adddir  33561  archiabl  33741  ssmxidl  33981  dimvalfi  34216  probun  35034  satfv1lem  36096  trisegint  36763  btwnconn1lem13  36834  brsegle2  36844  linethru  36888  lindsadd  38504  hlrelat  40427  intnatN  40432  lnnat  40452  3dim0  40482  3dim1  40492  3dim2  40493  atcvrlln  40545  llnexatN  40546  2at0mat0  40550  llncvrlpln  40583  lplnexllnN  40589  lplncvrlvol  40641  lncvrelatN  40806  lncmp  40808  elpaddn0  40825  paddasslem5  40849  pmapjoin  40877  pmapjat1  40878  pclclN  40916  osumclN  40992  lhprelat3N  41065  trlval4  41213  cdlemd5  41227  cdleme32fvcl  41465  cdleme42keg  41511  cdlemg1a  41595  cdlemg1cN  41612  cdlemg39  41741  ltrncom  41763  cdlemk34  41935  dihord2pre  42250  dihopelvalcpre  42273  dihmeetALTN  42352  dihlspsnssN  42357  dihlspsnat  42358  aks6d1c6isolem1  43192  diophrw  43723  lzunuz  43732  qirropth  43868  jm2.19  43953  jm2.27  43968  lmhmfgsplit  44046  hbtlem5  44088  nadd2rabtr  44344  fzunt  44414  iunrelexpuztr  44678  rfcnnnub  45996  3adantll2  46001  3adantll3  46002  ioondisj2  46449  ioondisj1  46450  iccintsng  46479  icccncfext  46841  stoweidlem20  46974  stoweidlem61  47015  smflimlem2  47726  isuspgrim0lem  48935  isuspgrim0  48936  rmsupp0  49424  rmsuppss  49426  ply1mulgsum  49446  rrxlinesc  49791