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  7259  poxp3  8129  naddsuc2  8665  ordiso2  9468  hartogslem1  9495  wemapso2lem  9505  acndom  10004  fin1a2lem12  10364  fin1a2lem13  10365  prlem934  10986  ifle  13157  lcmfunsnlem2lem1  16608  divgcdcoprm0  16635  rpexp  16692  qexpz  16872  ramval  16979  0ram  16991  ramz2  16995  initoeu2lem2  17977  mrelatglb  18519  dfgrp3lem  18970  odbezout  19488  rhmdvdsr  20417  lsmcl  20990  lbsextlem3  21070  rnglidlmcl  21126  frlmsslsp  21705  islindf4  21747  psropprmul  22122  coe1mul2  22155  coe1fzgsumdlem  22190  evl1gsumdlem  22243  scmate  22397  mdetunilem7  22505  mdetmul  22510  cramerlem2  22575  m2pmfzgsumcl  22635  decpmatmul  22659  pmatcollpw3lem  22670  chpdmatlem2  22726  cpmadugsumlemB  22761  cpmadugsumlemC  22762  cpmadugsumlemF  22763  chcoeffeqlem  22772  cnconst2  23170  ordthauslem  23270  clsconn  23317  restnlly  23369  comppfsc  23419  ptpjopn  23499  trfg  23778  rnelfmlem  23839  isfcf  23921  fcfnei  23922  cnpfcf  23928  utop2nei  24138  neipcfilu  24183  blssps  24312  blss  24313  metcnp  24429  xrsxmet  24698  metdsge  24738  metdseq0  24743  addcnlem  24753  xrhmeo  24844  nmhmcn  25020  caucfil  25183  limcfval  25773  fta1b  26077  lgsmod  27234  lgsdir  27243  lgsne0  27246  nosupbnd1lem3  27622  nosupbnd1lem4  27623  nosupbnd1lem5  27624  nosupbnd2  27628  noinfbnd1lem3  27637  noinfbnd1lem4  27638  noinfbnd1lem5  27639  noinfbnd2  27643  scutun12  27722  sltlpss  27819  sleadd1  27896  axpasch  28868  axcontlem2  28892  clwwlknonex2  30038  frgr3v  30204  pjhthmo  31231  difioo  32705  xrge0adddir  32959  archiabl  33152  ssmxidl  33445  dimvalfi  33597  probun  34410  satfv1lem  35349  trisegint  36016  btwnconn1lem13  36087  brsegle2  36097  linethru  36141  lindsadd  37607  hlrelat  39396  intnatN  39401  lnnat  39421  3dim0  39451  3dim1  39461  3dim2  39462  atcvrlln  39514  llnexatN  39515  2at0mat0  39519  llncvrlpln  39552  lplnexllnN  39558  lplncvrlvol  39610  lncvrelatN  39775  lncmp  39777  elpaddn0  39794  paddasslem5  39818  pmapjoin  39846  pmapjat1  39847  pclclN  39885  osumclN  39961  lhprelat3N  40034  trlval4  40182  cdlemd5  40196  cdleme32fvcl  40434  cdleme42keg  40480  cdlemg1a  40564  cdlemg1cN  40581  cdlemg39  40710  ltrncom  40732  cdlemk34  40904  dihord2pre  41219  dihopelvalcpre  41242  dihmeetALTN  41321  dihlspsnssN  41326  dihlspsnat  41327  aks6d1c6isolem1  42162  diophrw  42747  lzunuz  42756  qirropth  42896  jm2.19  42982  jm2.27  42997  lmhmfgsplit  43075  hbtlem5  43117  nadd2rabtr  43373  fzunt  43444  iunrelexpuztr  43708  rfcnnnub  45030  3adantll2  45035  3adantll3  45036  ioondisj2  45491  ioondisj1  45492  iccintsng  45521  icccncfext  45885  stoweidlem20  46018  stoweidlem61  46059  smflimlem2  46770  isuspgrim0lem  47893  isuspgrim0  47894  rmsupp0  48356  rmsuppss  48358  ply1mulgsum  48379  rrxlinesc  48724