Theorem simpll1 1225

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  f1prex  7264  poxp3  8125  naddsuc2  8667  ordiso2  9460  hartogslem1  9487  wemapso2lem  9497  acndom  10004  fin1a2lem12  10365  fin1a2lem13  10366  prlem934  10988  ifle  13197  lcmfunsnlem2lem1  16655  divgcdcoprm0  16682  rpexp  16740  qexpz  16920  ramval  17027  0ram  17039  ramz2  17043  initoeu2lem2  18031  mrelatglb  18575  dfgrp3lem  19063  odbezout  19581  rhmdvdsr  20537  lsmcl  21130  lbsextlem3  21210  rnglidlmcl  21266  frlmsslsp  21828  islindf4  21870  psropprmul  22279  coe1mul2  22312  coe1fzgsumdlem  22346  evl1gsumdlem  22399  scmate  22550  mdetunilem7  22658  mdetmul  22663  cramerlem2  22728  m2pmfzgsumcl  22788  decpmatmul  22812  pmatcollpw3lem  22823  chpdmatlem2  22879  cpmadugsumlemB  22914  cpmadugsumlemC  22915  cpmadugsumlemF  22916  chcoeffeqlem  22925  cnconst2  23323  ordthauslem  23423  clsconn  23470  restnlly  23522  comppfsc  23572  ptpjopn  23652  trfg  23931  rnelfmlem  23992  isfcf  24074  fcfnei  24075  cnpfcf  24081  utop2nei  24290  neipcfilu  24335  blssps  24464  blss  24465  metcnp  24581  xrsxmet  24850  metdsge  24890  metdseq0  24895  addcnlem  24905  xrhmeo  24988  nmhmcn  25162  caucfil  25325  limcfval  25914  fta1b  26212  lgsmod  27364  lgsdir  27373  lgsne0  27376  nosupbnd1lem3  27751  nosupbnd1lem4  27752  nosupbnd1lem5  27753  nosupbnd2  27757  noinfbnd1lem3  27766  noinfbnd1lem4  27767  noinfbnd1lem5  27768  noinfbnd2  27772  cutsun12  27860  ltslpss  27978  leadds1  28059  axpasch  29088  axcontlem2  29112  clwwlknonex2  30257  frgr3v  30423  pjhthmo  31451  difioo  32934  xrge0adddir  33157  archiabl  33339  ssmxidl  33623  dimvalfi  33860  probun  34677  satfv1lem  35676  trisegint  36342  btwnconn1lem13  36413  brsegle2  36423  linethru  36467  lindsadd  38076  hlrelat  39990  intnatN  39995  lnnat  40015  3dim0  40045  3dim1  40055  3dim2  40056  atcvrlln  40108  llnexatN  40109  2at0mat0  40113  llncvrlpln  40146  lplnexllnN  40152  lplncvrlvol  40204  lncvrelatN  40369  lncmp  40371  elpaddn0  40388  paddasslem5  40412  pmapjoin  40440  pmapjat1  40441  pclclN  40479  osumclN  40555  lhprelat3N  40628  trlval4  40776  cdlemd5  40790  cdleme32fvcl  41028  cdleme42keg  41074  cdlemg1a  41158  cdlemg1cN  41175  cdlemg39  41304  ltrncom  41326  cdlemk34  41498  dihord2pre  41813  dihopelvalcpre  41836  dihmeetALTN  41915  dihlspsnssN  41920  dihlspsnat  41921  aks6d1c6isolem1  42755  diophrw  43304  lzunuz  43313  qirropth  43449  jm2.19  43534  jm2.27  43549  lmhmfgsplit  43627  hbtlem5  43669  nadd2rabtr  43925  fzunt  43995  iunrelexpuztr  44259  rfcnnnub  45580  3adantll2  45585  3adantll3  45586  ioondisj2  46033  ioondisj1  46034  iccintsng  46063  icccncfext  46425  stoweidlem20  46558  stoweidlem61  46599  smflimlem2  47310  isuspgrim0lem  48479  isuspgrim0  48480  rmsupp0  48954  rmsuppss  48956  ply1mulgsum  48976  rrxlinesc  49321