Theorem simpll1 1210

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1085

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 395  df-3an 1087

This theorem is referenced by:  f1prex  7284  poxp3  8138  ordiso2  9512  hartogslem1  9539  wemapso2lem  9549  acndom  10048  fin1a2lem12  10408  fin1a2lem13  10409  prlem934  11030  ifle  13180  lcmfunsnlem2lem1  16579  divgcdcoprm0  16606  rpexp  16663  qexpz  16838  ramval  16945  0ram  16957  ramz2  16961  initoeu2lem2  17969  mrelatglb  18517  dfgrp3lem  18957  odbezout  19467  rhmdvdsr  20399  lsmcl  20838  lbsextlem3  20918  rnglidlmcl  20982  frlmsslsp  21570  islindf4  21612  psropprmul  21980  coe1mul2  22011  coe1fzgsumdlem  22045  evl1gsumdlem  22095  scmate  22232  mdetunilem7  22340  mdetmul  22345  cramerlem2  22410  m2pmfzgsumcl  22470  decpmatmul  22494  pmatcollpw3lem  22505  chpdmatlem2  22561  cpmadugsumlemB  22596  cpmadugsumlemC  22597  cpmadugsumlemF  22598  chcoeffeqlem  22607  cnconst2  23007  ordthauslem  23107  clsconn  23154  restnlly  23206  comppfsc  23256  ptpjopn  23336  trfg  23615  rnelfmlem  23676  isfcf  23758  fcfnei  23759  cnpfcf  23765  utop2nei  23975  neipcfilu  24021  blssps  24150  blss  24151  metcnp  24270  xrsxmet  24545  metdsge  24585  metdseq0  24590  addcnlem  24600  xrhmeo  24691  nmhmcn  24867  caucfil  25031  limcfval  25621  fta1b  25922  lgsmod  27062  lgsdir  27071  lgsne0  27074  nosupbnd1lem3  27449  nosupbnd1lem4  27450  nosupbnd1lem5  27451  nosupbnd2  27455  noinfbnd1lem3  27464  noinfbnd1lem4  27465  noinfbnd1lem5  27466  noinfbnd2  27470  scutun12  27548  sltlpss  27638  sleadd1  27711  axpasch  28466  axcontlem2  28490  clwwlknonex2  29629  frgr3v  29795  pjhthmo  30822  difioo  32260  xrge0adddir  32460  archiabl  32614  ssmxidl  32864  dimvalfi  32974  probun  33716  satfv1lem  34651  trisegint  35304  btwnconn1lem13  35375  brsegle2  35385  linethru  35429  lindsadd  36784  hlrelat  38576  intnatN  38581  lnnat  38601  3dim0  38631  3dim1  38641  3dim2  38642  atcvrlln  38694  llnexatN  38695  2at0mat0  38699  llncvrlpln  38732  lplnexllnN  38738  lplncvrlvol  38790  lncvrelatN  38955  lncmp  38957  elpaddn0  38974  paddasslem5  38998  pmapjoin  39026  pmapjat1  39027  pclclN  39065  osumclN  39141  lhprelat3N  39214  trlval4  39362  cdlemd5  39376  cdleme32fvcl  39614  cdleme42keg  39660  cdlemg1a  39744  cdlemg1cN  39761  cdlemg39  39890  ltrncom  39912  cdlemk34  40084  dihord2pre  40399  dihopelvalcpre  40422  dihmeetALTN  40501  dihlspsnssN  40506  dihlspsnat  40507  diophrw  41799  lzunuz  41808  qirropth  41948  jm2.19  42034  jm2.27  42049  lmhmfgsplit  42130  hbtlem5  42172  nadd2rabtr  42436  naddsuc2  42445  fzunt  42508  iunrelexpuztr  42772  rfcnnnub  44022  3adantll2  44027  3adantll3  44028  ioondisj2  44504  ioondisj1  44505  iccintsng  44534  icccncfext  44901  stoweidlem20  45034  stoweidlem61  45075  smflimlem2  45786  rmsupp0  47132  rmsuppss  47134  ply1mulgsum  47158  rrxlinesc  47508