Theorem simpll1 1231

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  f1prex  7292  poxp3  8169  naddsuc2  8714  ordiso2  9512  hartogslem1  9539  wemapso2lem  9549  acndom  10133  fin1a2lem12  10492  fin1a2lem13  10493  prlem934  11121  ifle  13330  lcmfunsnlem2lem1  16818  divgcdcoprm0  16845  rpexp  16903  qexpz  17084  ramval  17191  0ram  17203  ramz2  17207  initoeu2lem2  18195  mrelatglb  18739  dfgrp3lem  19253  odbezout  19777  rhmdvdsr  20763  lsmcl  21363  lbsextlem3  21443  rnglidlmcl  21500  frlmsslsp  22107  islindf4  22149  psropprmul  22560  coe1mul2  22593  coe1fzgsumdlem  22626  evl1gsumdlem  22679  scmate  22830  mdetunilem7  22938  mdetmul  22943  cramerlem2  23011  m2pmfzgsumcl  23071  decpmatmul  23095  pmatcollpw3lem  23106  chpdmatlem2  23162  cpmadugsumlemB  23197  cpmadugsumlemC  23198  cpmadugsumlemF  23199  chcoeffeqlem  23208  cnconst2  23606  ordthauslem  23706  clsconn  23753  restnlly  23806  comppfsc  23856  ptpjopn  23936  trfg  24215  rnelfmlem  24276  isfcf  24358  fcfnei  24359  cnpfcf  24365  utop2nei  24574  neipcfilu  24619  blssps  24748  blss  24749  metcnp  24865  xrsxmet  25134  metdsge  25174  metdseq0  25179  addcnlem  25189  xrhmeo  25272  nmhmcn  25446  caucfil  25609  limcfval  26197  fta1b  26495  lgsmod  27655  lgsdir  27664  lgsne0  27667  nosupbnd1lem3  28072  nosupbnd1lem4  28073  nosupbnd1lem5  28074  nosupbnd2  28078  noinfbnd1lem3  28087  noinfbnd1lem4  28088  noinfbnd1lem5  28089  noinfbnd2  28093  cutsun12  28181  ltslpss  28299  leadds1  28380  axpasch  29524  axcontlem2  29548  clwwlknonex2  30705  frgr3v  30881  pjhthmo  31909  difioo  33420  xrge0adddir  33625  archiabl  33805  ssmxidl  34045  dimvalfi  34280  probun  35097  satfv1lem  36213  trisegint  36885  btwnconn1lem13  36956  brsegle2  36966  linethru  37010  lindsadd  38629  hlrelat  40552  intnatN  40557  lnnat  40577  3dim0  40607  3dim1  40617  3dim2  40618  atcvrlln  40670  llnexatN  40671  2at0mat0  40675  llncvrlpln  40708  lplnexllnN  40714  lplncvrlvol  40766  lncvrelatN  40931  lncmp  40933  elpaddn0  40950  paddasslem5  40974  pmapjoin  41002  pmapjat1  41003  pclclN  41041  osumclN  41117  lhprelat3N  41190  trlval4  41338  cdlemd5  41352  cdleme32fvcl  41590  cdleme42keg  41636  cdlemg1a  41720  cdlemg1cN  41737  cdlemg39  41866  ltrncom  41888  cdlemk34  42060  dihord2pre  42375  dihopelvalcpre  42398  dihmeetALTN  42477  dihlspsnssN  42482  dihlspsnat  42483  aks6d1c6isolem1  43317  diophrw  43863  lzunuz  43872  qirropth  44008  jm2.19  44093  jm2.27  44108  lmhmfgsplit  44181  hbtlem5  44223  nadd2rabtr  44479  fzunt  44549  iunrelexpuztr  44812  rfcnnnub  46146  3adantll2  46151  3adantll3  46152  ioondisj2  46598  ioondisj1  46599  iccintsng  46628  icccncfext  46990  stoweidlem20  47123  stoweidlem61  47164  smflimlem2  47875  isuspgrim0lem  49084  isuspgrim0  49085  rmsupp0  49573  rmsuppss  49575  ply1mulgsum  49595  rrxlinesc  49941