Theorem simpll3 1231

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)

Assertion

Ref	Expression
simpll3	⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜒)

Proof of Theorem simpll3

Step	Hyp	Ref	Expression
1		simp3 1154	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒)
2	1	ad2antrr 738	1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  f1prex  7272  poxp3  8134  naddsuc2  8676  ordiso2  9465  iunfictbso  10086  fin1a2lem12  10383  fin1a2lem13  10384  prlem934  11006  ifle  13214  xlesubadd  13280  icoshftf1o  13492  elfzonelfzo  13789  fsuppmapnn0fiub0  14020  swrdcl  14673  repswccat  14813  subcn2  15636  rpdvds  16708  coprmprod  16709  qexpz  16951  ramval  17058  0ram  17070  cshwrepswhash1  17152  mreexexd  17694  gsmsymgreqlem1  19491  pmtrf  19516  odmulg  19617  pgpfi1  19656  lsmcl  21173  lbsextlem3  21253  islindf4  21948  coe1mul2  22390  cramerlem2  22806  cpmadugsumlemF  22994  cayhamlem4  23006  iscnp4  23381  cnpnei  23382  cnconst2  23401  cnpdis  23411  cnhaus  23472  ordthauslem  23501  clsconn  23548  nlly2i  23594  txcn  23744  ordthmeolem  23919  flimrest  24101  isfcf  24152  alexsubALTlem4  24168  ghmcnp  24233  utop2nei  24368  blssps  24542  blss  24543  metcnp3  24658  metcnp  24659  xrsxmet  24928  metdseq0  24973  xrhmeo  25066  cfil3i  25389  caucfil  25403  cfilres  25416  fta1b  26290  mumul  27303  lgsfcl2  27425  lgsdir  27454  lgsne0  27457  nolt02o  27817  nogt01o  27818  nosupbnd1lem3  27832  nosupbnd1lem4  27833  nosupbnd1lem5  27834  nosupbnd2  27838  noinfbnd1lem3  27847  noinfbnd1lem4  27848  noinfbnd1lem5  27849  noinfbnd2  27853  leadds1  28140  ltmuls2  28322  istrkgcb  28683  axbtwnid  29198  axcontlem2  29224  axcontlem4  29226  axcontlem7  29229  axcontlem8  29230  umgr2v2enb1  29785  frgr3v  30535  extwwlkfab  30612  pjhthmo  31563  xrge0adddir  33251  archiabl  33431  dimvalfi  33909  pcmplfinf  34168  probun  34726  cnpconn  35593  satfv1lem  35725  outsideofeq  36493  linethru  36516  weiunso  36839  atlatmstc  39955  cvlcvr1  39975  ishlat3N  39990  hlrelat  40038  intnatN  40043  cvrval5  40051  atcvrlln  40156  llnexatN  40157  2at0mat0  40161  llncvrlpln  40194  lplnexllnN  40200  lplncvrlvol  40252  lncvrelatN  40417  pmapjoin  40488  pmapjat1  40489  pclclN  40527  osumclN  40603  lhprelat3N  40676  cdlemd5  40838  cdleme32fvcl  41076  cdlemg39  41352  ltrncom  41374  dihmeetALTN  41963  dochss  42001  mapdrvallem2  42281  nacsfix  43305  mzpsubst  43341  diophrw  43352  lzunuz  43361  jm2.19  43582  jm2.27  43597  hbtlem5  43717  tfsconcatrn  43931  nadd2rabtr  43973  fzunt  44043  iunrelexpuztr  44307  grumnudlem  44859  rfcnnnub  45614  3adantll2  45619  infleinf  45945  iccintsng  46097  mullimc  46190  mullimcf  46197  limcperiod  46202  cncfshift  46446  cncfperiod  46451  icccncfext  46459  stoweidlem20  46592  stoweidlem61  46633  fourierdlem73  46751  rmsupp0  48999  rmsuppss  49001  itschlc0xyqsol1  49397  itschlc0xyqsol  49398