Theorem simpll3 1233

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 1156	. 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  7285  poxp3  8148  naddsuc2  8690  ordiso2  9487  iunfictbso  10117  fin1a2lem12  10413  fin1a2lem13  10414  prlem934  11042  ifle  13249  xlesubadd  13315  icoshftf1o  13527  elfzonelfzo  13825  fsuppmapnn0fiub0  14057  swrdcl  14713  repswccat  14857  subcn2  15682  rpdvds  16750  coprmprod  16751  qexpz  16993  ramval  17100  0ram  17112  cshwrepswhash1  17194  mreexexd  17736  gsmsymgreqlem1  19557  pmtrf  19582  odmulg  19683  pgpfi1  19722  lsmcl  21267  lbsextlem3  21347  islindf4  22051  coe1mul2  22495  cramerlem2  22913  cpmadugsumlemF  23101  cayhamlem4  23113  iscnp4  23488  cnpnei  23489  cnconst2  23508  cnpdis  23518  cnhaus  23579  ordthauslem  23608  clsconn  23655  nlly2i  23702  txcn  23852  ordthmeolem  24027  flimrest  24209  isfcf  24260  alexsubALTlem4  24276  ghmcnp  24341  utop2nei  24476  blssps  24650  blss  24651  metcnp3  24766  metcnp  24767  xrsxmet  25036  metdseq0  25081  xrhmeo  25174  cfil3i  25497  caucfil  25511  cfilres  25524  fta1b  26397  mumul  27417  lgsfcl2  27539  lgsdir  27568  lgsne0  27571  nolt02o  27931  nogt01o  27932  nosupbnd1lem3  27946  nosupbnd1lem4  27947  nosupbnd1lem5  27948  nosupbnd2  27952  noinfbnd1lem3  27961  noinfbnd1lem4  27962  noinfbnd1lem5  27963  noinfbnd2  27967  leadds1  28254  ltmuls2  28436  istrkgcb  28797  axbtwnid  29396  axcontlem2  29422  axcontlem4  29424  axcontlem7  29427  axcontlem8  29428  umgr2v2enb1  29986  frgr3v  30755  extwwlkfab  30832  pjhthmo  31783  xrge0adddir  33458  archiabl  33638  dimvalfi  34112  pcmplfinf  34371  probun  34930  cnpconn  35809  satfv1lem  35941  outsideofeq  36710  linethru  36733  weiunso  37085  atlatmstc  40192  cvlcvr1  40212  ishlat3N  40227  hlrelat  40275  intnatN  40280  cvrval5  40288  atcvrlln  40393  llnexatN  40394  2at0mat0  40398  llncvrlpln  40431  lplnexllnN  40437  lplncvrlvol  40489  lncvrelatN  40654  pmapjoin  40725  pmapjat1  40726  pclclN  40764  osumclN  40840  lhprelat3N  40913  cdlemd5  41075  cdleme32fvcl  41313  cdlemg39  41589  ltrncom  41611  dihmeetALTN  42200  dochss  42238  mapdrvallem2  42518  nacsfix  43557  mzpsubst  43593  diophrw  43604  lzunuz  43613  jm2.19  43834  jm2.27  43849  hbtlem5  43969  tfsconcatrn  44183  nadd2rabtr  44225  fzunt  44295  iunrelexpuztr  44559  grumnudlem  45109  rfcnnnub  45870  3adantll2  45875  infleinf  46201  iccintsng  46353  mullimc  46446  mullimcf  46453  limcperiod  46458  cncfshift  46702  cncfperiod  46707  icccncfext  46715  stoweidlem20  46848  stoweidlem61  46889  fourierdlem73  47007  rmsupp0  49298  rmsuppss  49300  itschlc0xyqsol1  49696  itschlc0xyqsol  49697