Theorem simpll1 1214

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 727	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  7232  poxp3  8093  naddsuc2  8630  ordiso2  9423  hartogslem1  9450  wemapso2lem  9460  acndom  9964  fin1a2lem12  10324  fin1a2lem13  10325  prlem934  10947  ifle  13140  lcmfunsnlem2lem1  16598  divgcdcoprm0  16625  rpexp  16683  qexpz  16863  ramval  16970  0ram  16982  ramz2  16986  initoeu2lem2  17973  mrelatglb  18517  dfgrp3lem  19005  odbezout  19524  rhmdvdsr  20476  lsmcl  21070  lbsextlem3  21150  rnglidlmcl  21206  frlmsslsp  21786  islindf4  21828  psropprmul  22211  coe1mul2  22244  coe1fzgsumdlem  22278  evl1gsumdlem  22331  scmate  22485  mdetunilem7  22593  mdetmul  22598  cramerlem2  22663  m2pmfzgsumcl  22723  decpmatmul  22747  pmatcollpw3lem  22758  chpdmatlem2  22814  cpmadugsumlemB  22849  cpmadugsumlemC  22850  cpmadugsumlemF  22851  chcoeffeqlem  22860  cnconst2  23258  ordthauslem  23358  clsconn  23405  restnlly  23457  comppfsc  23507  ptpjopn  23587  trfg  23866  rnelfmlem  23927  isfcf  24009  fcfnei  24010  cnpfcf  24016  utop2nei  24225  neipcfilu  24270  blssps  24399  blss  24400  metcnp  24516  xrsxmet  24785  metdsge  24825  metdseq0  24830  addcnlem  24840  xrhmeo  24923  nmhmcn  25097  caucfil  25260  limcfval  25849  fta1b  26147  lgsmod  27300  lgsdir  27309  lgsne0  27312  nosupbnd1lem3  27688  nosupbnd1lem4  27689  nosupbnd1lem5  27690  nosupbnd2  27694  noinfbnd1lem3  27703  noinfbnd1lem4  27704  noinfbnd1lem5  27705  noinfbnd2  27709  cutsun12  27796  ltslpss  27914  leadds1  27995  axpasch  29024  axcontlem2  29048  clwwlknonex2  30194  frgr3v  30360  pjhthmo  31388  difioo  32870  xrge0adddir  33093  archiabl  33274  ssmxidl  33549  dimvalfi  33761  probun  34579  satfv1lem  35560  trisegint  36226  btwnconn1lem13  36297  brsegle2  36307  linethru  36351  lindsadd  37948  hlrelat  39862  intnatN  39867  lnnat  39887  3dim0  39917  3dim1  39927  3dim2  39928  atcvrlln  39980  llnexatN  39981  2at0mat0  39985  llncvrlpln  40018  lplnexllnN  40024  lplncvrlvol  40076  lncvrelatN  40241  lncmp  40243  elpaddn0  40260  paddasslem5  40284  pmapjoin  40312  pmapjat1  40313  pclclN  40351  osumclN  40427  lhprelat3N  40500  trlval4  40648  cdlemd5  40662  cdleme32fvcl  40900  cdleme42keg  40946  cdlemg1a  41030  cdlemg1cN  41047  cdlemg39  41176  ltrncom  41198  cdlemk34  41370  dihord2pre  41685  dihopelvalcpre  41708  dihmeetALTN  41787  dihlspsnssN  41792  dihlspsnat  41793  aks6d1c6isolem1  42627  diophrw  43205  lzunuz  43214  qirropth  43354  jm2.19  43439  jm2.27  43454  lmhmfgsplit  43532  hbtlem5  43574  nadd2rabtr  43830  fzunt  43900  iunrelexpuztr  44164  rfcnnnub  45485  3adantll2  45490  3adantll3  45491  ioondisj2  45941  ioondisj1  45942  iccintsng  45971  icccncfext  46333  stoweidlem20  46466  stoweidlem61  46507  smflimlem2  47218  isuspgrim0lem  48381  isuspgrim0  48382  rmsupp0  48856  rmsuppss  48858  ply1mulgsum  48878  rrxlinesc  49223