Theorem simpll1 1213

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  f1prex  7304  poxp3  8175  naddsuc2  8739  ordiso2  9555  hartogslem1  9582  wemapso2lem  9592  acndom  10091  fin1a2lem12  10451  fin1a2lem13  10452  prlem934  11073  ifle  13239  lcmfunsnlem2lem1  16675  divgcdcoprm0  16702  rpexp  16759  qexpz  16939  ramval  17046  0ram  17058  ramz2  17062  initoeu2lem2  18060  mrelatglb  18605  dfgrp3lem  19056  odbezout  19576  rhmdvdsr  20508  lsmcl  21082  lbsextlem3  21162  rnglidlmcl  21226  frlmsslsp  21816  islindf4  21858  psropprmul  22239  coe1mul2  22272  coe1fzgsumdlem  22307  evl1gsumdlem  22360  scmate  22516  mdetunilem7  22624  mdetmul  22629  cramerlem2  22694  m2pmfzgsumcl  22754  decpmatmul  22778  pmatcollpw3lem  22789  chpdmatlem2  22845  cpmadugsumlemB  22880  cpmadugsumlemC  22881  cpmadugsumlemF  22882  chcoeffeqlem  22891  cnconst2  23291  ordthauslem  23391  clsconn  23438  restnlly  23490  comppfsc  23540  ptpjopn  23620  trfg  23899  rnelfmlem  23960  isfcf  24042  fcfnei  24043  cnpfcf  24049  utop2nei  24259  neipcfilu  24305  blssps  24434  blss  24435  metcnp  24554  xrsxmet  24831  metdsge  24871  metdseq0  24876  addcnlem  24886  xrhmeo  24977  nmhmcn  25153  caucfil  25317  limcfval  25907  fta1b  26211  lgsmod  27367  lgsdir  27376  lgsne0  27379  nosupbnd1lem3  27755  nosupbnd1lem4  27756  nosupbnd1lem5  27757  nosupbnd2  27761  noinfbnd1lem3  27770  noinfbnd1lem4  27771  noinfbnd1lem5  27772  noinfbnd2  27776  scutun12  27855  sltlpss  27945  sleadd1  28022  axpasch  28956  axcontlem2  28980  clwwlknonex2  30128  frgr3v  30294  pjhthmo  31321  difioo  32784  xrge0adddir  33023  archiabl  33205  ssmxidl  33502  dimvalfi  33652  probun  34421  satfv1lem  35367  trisegint  36029  btwnconn1lem13  36100  brsegle2  36110  linethru  36154  lindsadd  37620  hlrelat  39404  intnatN  39409  lnnat  39429  3dim0  39459  3dim1  39469  3dim2  39470  atcvrlln  39522  llnexatN  39523  2at0mat0  39527  llncvrlpln  39560  lplnexllnN  39566  lplncvrlvol  39618  lncvrelatN  39783  lncmp  39785  elpaddn0  39802  paddasslem5  39826  pmapjoin  39854  pmapjat1  39855  pclclN  39893  osumclN  39969  lhprelat3N  40042  trlval4  40190  cdlemd5  40204  cdleme32fvcl  40442  cdleme42keg  40488  cdlemg1a  40572  cdlemg1cN  40589  cdlemg39  40718  ltrncom  40740  cdlemk34  40912  dihord2pre  41227  dihopelvalcpre  41250  dihmeetALTN  41329  dihlspsnssN  41334  dihlspsnat  41335  aks6d1c6isolem1  42175  diophrw  42770  lzunuz  42779  qirropth  42919  jm2.19  43005  jm2.27  43020  lmhmfgsplit  43098  hbtlem5  43140  nadd2rabtr  43397  fzunt  43468  iunrelexpuztr  43732  rfcnnnub  45041  3adantll2  45046  3adantll3  45047  ioondisj2  45506  ioondisj1  45507  iccintsng  45536  icccncfext  45902  stoweidlem20  46035  stoweidlem61  46076  smflimlem2  46787  isuspgrim0lem  47871  isuspgrim0  47872  rmsupp0  48284  rmsuppss  48286  ply1mulgsum  48307  rrxlinesc  48656