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  7218  poxp3  8080  naddsuc2  8616  ordiso2  9401  hartogslem1  9428  wemapso2lem  9438  acndom  9942  fin1a2lem12  10302  fin1a2lem13  10303  prlem934  10924  ifle  13096  lcmfunsnlem2lem1  16549  divgcdcoprm0  16576  rpexp  16633  qexpz  16813  ramval  16920  0ram  16932  ramz2  16936  initoeu2lem2  17922  mrelatglb  18466  dfgrp3lem  18951  odbezout  19470  rhmdvdsr  20423  lsmcl  21017  lbsextlem3  21097  rnglidlmcl  21153  frlmsslsp  21733  islindf4  21775  psropprmul  22150  coe1mul2  22183  coe1fzgsumdlem  22218  evl1gsumdlem  22271  scmate  22425  mdetunilem7  22533  mdetmul  22538  cramerlem2  22603  m2pmfzgsumcl  22663  decpmatmul  22687  pmatcollpw3lem  22698  chpdmatlem2  22754  cpmadugsumlemB  22789  cpmadugsumlemC  22790  cpmadugsumlemF  22791  chcoeffeqlem  22800  cnconst2  23198  ordthauslem  23298  clsconn  23345  restnlly  23397  comppfsc  23447  ptpjopn  23527  trfg  23806  rnelfmlem  23867  isfcf  23949  fcfnei  23950  cnpfcf  23956  utop2nei  24165  neipcfilu  24210  blssps  24339  blss  24340  metcnp  24456  xrsxmet  24725  metdsge  24765  metdseq0  24770  addcnlem  24780  xrhmeo  24871  nmhmcn  25047  caucfil  25210  limcfval  25800  fta1b  26104  lgsmod  27261  lgsdir  27270  lgsne0  27273  nosupbnd1lem3  27649  nosupbnd1lem4  27650  nosupbnd1lem5  27651  nosupbnd2  27655  noinfbnd1lem3  27664  noinfbnd1lem4  27665  noinfbnd1lem5  27666  noinfbnd2  27670  scutun12  27751  sltlpss  27853  sleadd1  27932  axpasch  28919  axcontlem2  28943  clwwlknonex2  30089  frgr3v  30255  pjhthmo  31282  difioo  32765  xrge0adddir  32999  archiabl  33167  ssmxidl  33439  dimvalfi  33614  probun  34432  satfv1lem  35406  trisegint  36072  btwnconn1lem13  36143  brsegle2  36153  linethru  36197  lindsadd  37652  hlrelat  39500  intnatN  39505  lnnat  39525  3dim0  39555  3dim1  39565  3dim2  39566  atcvrlln  39618  llnexatN  39619  2at0mat0  39623  llncvrlpln  39656  lplnexllnN  39662  lplncvrlvol  39714  lncvrelatN  39879  lncmp  39881  elpaddn0  39898  paddasslem5  39922  pmapjoin  39950  pmapjat1  39951  pclclN  39989  osumclN  40065  lhprelat3N  40138  trlval4  40286  cdlemd5  40300  cdleme32fvcl  40538  cdleme42keg  40584  cdlemg1a  40668  cdlemg1cN  40685  cdlemg39  40814  ltrncom  40836  cdlemk34  41008  dihord2pre  41323  dihopelvalcpre  41346  dihmeetALTN  41425  dihlspsnssN  41430  dihlspsnat  41431  aks6d1c6isolem1  42266  diophrw  42851  lzunuz  42860  qirropth  43000  jm2.19  43085  jm2.27  43100  lmhmfgsplit  43178  hbtlem5  43220  nadd2rabtr  43476  fzunt  43547  iunrelexpuztr  43811  rfcnnnub  45132  3adantll2  45137  3adantll3  45138  ioondisj2  45592  ioondisj1  45593  iccintsng  45622  icccncfext  45984  stoweidlem20  46117  stoweidlem61  46158  smflimlem2  46869  isuspgrim0lem  47992  isuspgrim0  47993  rmsupp0  48467  rmsuppss  48469  ply1mulgsum  48490  rrxlinesc  48835