Theorem simpll1 1209

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084

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 395  df-3an 1086

This theorem is referenced by:  f1prex  7293  poxp3  8155  ordiso2  9540  hartogslem1  9567  wemapso2lem  9577  acndom  10076  fin1a2lem12  10436  fin1a2lem13  10437  prlem934  11058  ifle  13211  lcmfunsnlem2lem1  16612  divgcdcoprm0  16639  rpexp  16697  qexpz  16873  ramval  16980  0ram  16992  ramz2  16996  initoeu2lem2  18007  mrelatglb  18555  dfgrp3lem  19002  odbezout  19525  rhmdvdsr  20459  lsmcl  20980  lbsextlem3  21060  rnglidlmcl  21124  frlmsslsp  21747  islindf4  21789  psropprmul  22180  coe1mul2  22213  coe1fzgsumdlem  22247  evl1gsumdlem  22300  scmate  22456  mdetunilem7  22564  mdetmul  22569  cramerlem2  22634  m2pmfzgsumcl  22694  decpmatmul  22718  pmatcollpw3lem  22729  chpdmatlem2  22785  cpmadugsumlemB  22820  cpmadugsumlemC  22821  cpmadugsumlemF  22822  chcoeffeqlem  22831  cnconst2  23231  ordthauslem  23331  clsconn  23378  restnlly  23430  comppfsc  23480  ptpjopn  23560  trfg  23839  rnelfmlem  23900  isfcf  23982  fcfnei  23983  cnpfcf  23989  utop2nei  24199  neipcfilu  24245  blssps  24374  blss  24375  metcnp  24494  xrsxmet  24769  metdsge  24809  metdseq0  24814  addcnlem  24824  xrhmeo  24915  nmhmcn  25091  caucfil  25255  limcfval  25845  fta1b  26151  lgsmod  27301  lgsdir  27310  lgsne0  27313  nosupbnd1lem3  27689  nosupbnd1lem4  27690  nosupbnd1lem5  27691  nosupbnd2  27695  noinfbnd1lem3  27704  noinfbnd1lem4  27705  noinfbnd1lem5  27706  noinfbnd2  27710  scutun12  27789  sltlpss  27879  sleadd1  27952  axpasch  28824  axcontlem2  28848  clwwlknonex2  29991  frgr3v  30157  pjhthmo  31184  difioo  32632  xrge0adddir  32837  archiabl  32998  ssmxidl  33286  dimvalfi  33430  probun  34170  satfv1lem  35103  trisegint  35755  btwnconn1lem13  35826  brsegle2  35836  linethru  35880  lindsadd  37217  hlrelat  39005  intnatN  39010  lnnat  39030  3dim0  39060  3dim1  39070  3dim2  39071  atcvrlln  39123  llnexatN  39124  2at0mat0  39128  llncvrlpln  39161  lplnexllnN  39167  lplncvrlvol  39219  lncvrelatN  39384  lncmp  39386  elpaddn0  39403  paddasslem5  39427  pmapjoin  39455  pmapjat1  39456  pclclN  39494  osumclN  39570  lhprelat3N  39643  trlval4  39791  cdlemd5  39805  cdleme32fvcl  40043  cdleme42keg  40089  cdlemg1a  40173  cdlemg1cN  40190  cdlemg39  40319  ltrncom  40341  cdlemk34  40513  dihord2pre  40828  dihopelvalcpre  40851  dihmeetALTN  40930  dihlspsnssN  40935  dihlspsnat  40936  aks6d1c6isolem1  41777  diophrw  42321  lzunuz  42330  qirropth  42470  jm2.19  42556  jm2.27  42571  lmhmfgsplit  42652  hbtlem5  42694  nadd2rabtr  42955  naddsuc2  42964  fzunt  43027  iunrelexpuztr  43291  rfcnnnub  44540  3adantll2  44545  3adantll3  44546  ioondisj2  45016  ioondisj1  45017  iccintsng  45046  icccncfext  45413  stoweidlem20  45546  stoweidlem61  45587  smflimlem2  46298  isuspgrim0lem  47355  isuspgrim0  47356  rmsupp0  47618  rmsuppss  47620  ply1mulgsum  47644  rrxlinesc  47994