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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 1088

This theorem is referenced by:  f1prex  7262  poxp3  8132  naddsuc2  8668  ordiso2  9475  hartogslem1  9502  wemapso2lem  9512  acndom  10011  fin1a2lem12  10371  fin1a2lem13  10372  prlem934  10993  ifle  13164  lcmfunsnlem2lem1  16615  divgcdcoprm0  16642  rpexp  16699  qexpz  16879  ramval  16986  0ram  16998  ramz2  17002  initoeu2lem2  17984  mrelatglb  18526  dfgrp3lem  18977  odbezout  19495  rhmdvdsr  20424  lsmcl  20997  lbsextlem3  21077  rnglidlmcl  21133  frlmsslsp  21712  islindf4  21754  psropprmul  22129  coe1mul2  22162  coe1fzgsumdlem  22197  evl1gsumdlem  22250  scmate  22404  mdetunilem7  22512  mdetmul  22517  cramerlem2  22582  m2pmfzgsumcl  22642  decpmatmul  22666  pmatcollpw3lem  22677  chpdmatlem2  22733  cpmadugsumlemB  22768  cpmadugsumlemC  22769  cpmadugsumlemF  22770  chcoeffeqlem  22779  cnconst2  23177  ordthauslem  23277  clsconn  23324  restnlly  23376  comppfsc  23426  ptpjopn  23506  trfg  23785  rnelfmlem  23846  isfcf  23928  fcfnei  23929  cnpfcf  23935  utop2nei  24145  neipcfilu  24190  blssps  24319  blss  24320  metcnp  24436  xrsxmet  24705  metdsge  24745  metdseq0  24750  addcnlem  24760  xrhmeo  24851  nmhmcn  25027  caucfil  25190  limcfval  25780  fta1b  26084  lgsmod  27241  lgsdir  27250  lgsne0  27253  nosupbnd1lem3  27629  nosupbnd1lem4  27630  nosupbnd1lem5  27631  nosupbnd2  27635  noinfbnd1lem3  27644  noinfbnd1lem4  27645  noinfbnd1lem5  27646  noinfbnd2  27650  scutun12  27729  sltlpss  27826  sleadd1  27903  axpasch  28875  axcontlem2  28899  clwwlknonex2  30045  frgr3v  30211  pjhthmo  31238  difioo  32712  xrge0adddir  32966  archiabl  33159  ssmxidl  33452  dimvalfi  33604  probun  34417  satfv1lem  35356  trisegint  36023  btwnconn1lem13  36094  brsegle2  36104  linethru  36148  lindsadd  37614  hlrelat  39403  intnatN  39408  lnnat  39428  3dim0  39458  3dim1  39468  3dim2  39469  atcvrlln  39521  llnexatN  39522  2at0mat0  39526  llncvrlpln  39559  lplnexllnN  39565  lplncvrlvol  39617  lncvrelatN  39782  lncmp  39784  elpaddn0  39801  paddasslem5  39825  pmapjoin  39853  pmapjat1  39854  pclclN  39892  osumclN  39968  lhprelat3N  40041  trlval4  40189  cdlemd5  40203  cdleme32fvcl  40441  cdleme42keg  40487  cdlemg1a  40571  cdlemg1cN  40588  cdlemg39  40717  ltrncom  40739  cdlemk34  40911  dihord2pre  41226  dihopelvalcpre  41249  dihmeetALTN  41328  dihlspsnssN  41333  dihlspsnat  41334  aks6d1c6isolem1  42169  diophrw  42754  lzunuz  42763  qirropth  42903  jm2.19  42989  jm2.27  43004  lmhmfgsplit  43082  hbtlem5  43124  nadd2rabtr  43380  fzunt  43451  iunrelexpuztr  43715  rfcnnnub  45037  3adantll2  45042  3adantll3  45043  ioondisj2  45498  ioondisj1  45499  iccintsng  45528  icccncfext  45892  stoweidlem20  46025  stoweidlem61  46066  smflimlem2  46777  isuspgrim0lem  47897  isuspgrim0  47898  rmsupp0  48360  rmsuppss  48362  ply1mulgsum  48383  rrxlinesc  48728