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

This theorem is referenced by:  f1prex  7149  ordiso2  9235  hartogslem1  9262  wemapso2lem  9272  acndom  9791  fin1a2lem12  10151  fin1a2lem13  10152  prlem934  10773  ifle  12913  lcmfunsnlem2lem1  16324  divgcdcoprm0  16351  rpexp  16408  qexpz  16583  ramval  16690  0ram  16702  ramz2  16706  initoeu2lem2  17711  mrelatglb  18259  dfgrp3lem  18654  odbezout  19146  lsmcl  20326  lbsextlem3  20403  frlmsslsp  20984  islindf4  21026  psropprmul  21390  coe1mul2  21421  coe1fzgsumdlem  21453  evl1gsumdlem  21503  scmate  21640  mdetunilem7  21748  mdetmul  21753  cramerlem2  21818  m2pmfzgsumcl  21878  decpmatmul  21902  pmatcollpw3lem  21913  chpdmatlem2  21969  cpmadugsumlemB  22004  cpmadugsumlemC  22005  cpmadugsumlemF  22006  chcoeffeqlem  22015  cnconst2  22415  ordthauslem  22515  clsconn  22562  restnlly  22614  comppfsc  22664  ptpjopn  22744  trfg  23023  rnelfmlem  23084  isfcf  23166  fcfnei  23167  cnpfcf  23173  utop2nei  23383  neipcfilu  23429  blssps  23558  blss  23559  metcnp  23678  xrsxmet  23953  metdsge  23993  metdseq0  23998  addcnlem  24008  xrhmeo  24090  nmhmcn  24264  caucfil  24428  limcfval  25017  fta1b  25315  lgsmod  26452  lgsdir  26461  lgsne0  26464  axpasch  27290  axcontlem2  27314  clwwlknonex2  28452  frgr3v  28618  pjhthmo  29643  difioo  31082  xrge0adddir  31280  archiabl  31431  rhmdvdsr  31496  ssmxidl  31621  dimvalfi  31666  probun  32365  satfv1lem  33303  nosupbnd1lem3  33892  nosupbnd1lem4  33893  nosupbnd1lem5  33894  nosupbnd2  33898  noinfbnd1lem3  33907  noinfbnd1lem4  33908  noinfbnd1lem5  33909  noinfbnd2  33913  scutun12  33983  sltlpss  34066  trisegint  34309  btwnconn1lem13  34380  brsegle2  34390  linethru  34434  lindsadd  35749  hlrelat  37395  intnatN  37400  lnnat  37420  3dim0  37450  3dim1  37460  3dim2  37461  atcvrlln  37513  llnexatN  37514  2at0mat0  37518  llncvrlpln  37551  lplnexllnN  37557  lplncvrlvol  37609  lncvrelatN  37774  lncmp  37776  elpaddn0  37793  paddasslem5  37817  pmapjoin  37845  pmapjat1  37846  pclclN  37884  osumclN  37960  lhprelat3N  38033  trlval4  38181  cdlemd5  38195  cdleme32fvcl  38433  cdleme42keg  38479  cdlemg1a  38563  cdlemg1cN  38580  cdlemg39  38709  ltrncom  38731  cdlemk34  38903  dihord2pre  39218  dihopelvalcpre  39241  dihmeetALTN  39320  dihlspsnssN  39325  dihlspsnat  39326  diophrw  40561  lzunuz  40570  qirropth  40710  jm2.19  40795  jm2.27  40810  lmhmfgsplit  40891  hbtlem5  40933  iunrelexpuztr  41280  rfcnnnub  42532  3adantll2  42539  3adantll3  42540  ioondisj2  42985  ioondisj1  42986  iccintsng  43015  icccncfext  43382  stoweidlem20  43515  stoweidlem61  43556  smflimlem2  44258  rmsupp0  45656  rmsuppss  45658  ply1mulgsum  45683  rrxlinesc  46033