Theorem simpll3 1216

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  f1prex  7232  poxp3  8093  naddsuc2  8630  ordiso2  9423  iunfictbso  10027  fin1a2lem12  10324  fin1a2lem13  10325  prlem934  10947  ifle  13140  xlesubadd  13206  icoshftf1o  13418  elfzonelfzo  13715  fsuppmapnn0fiub0  13946  swrdcl  14599  repswccat  14739  subcn2  15548  rpdvds  16620  coprmprod  16621  qexpz  16863  ramval  16970  0ram  16982  cshwrepswhash1  17064  mreexexd  17605  gsmsymgreqlem1  19396  pmtrf  19421  odmulg  19522  pgpfi1  19561  lsmcl  21070  lbsextlem3  21150  islindf4  21828  coe1mul2  22244  cramerlem2  22663  cpmadugsumlemF  22851  cayhamlem4  22863  iscnp4  23238  cnpnei  23239  cnconst2  23258  cnpdis  23268  cnhaus  23329  ordthauslem  23358  clsconn  23405  nlly2i  23451  txcn  23601  ordthmeolem  23776  flimrest  23958  isfcf  24009  alexsubALTlem4  24025  ghmcnp  24090  utop2nei  24225  blssps  24399  blss  24400  metcnp3  24515  metcnp  24516  xrsxmet  24785  metdseq0  24830  xrhmeo  24923  cfil3i  25246  caucfil  25260  cfilres  25273  fta1b  26147  mumul  27158  lgsfcl2  27280  lgsdir  27309  lgsne0  27312  nolt02o  27673  nogt01o  27674  nosupbnd1lem3  27688  nosupbnd1lem4  27689  nosupbnd1lem5  27690  nosupbnd2  27694  noinfbnd1lem3  27703  noinfbnd1lem4  27704  noinfbnd1lem5  27705  noinfbnd2  27709  leadds1  27995  ltmuls2  28177  istrkgcb  28538  axbtwnid  29022  axcontlem2  29048  axcontlem4  29050  axcontlem7  29053  axcontlem8  29054  umgr2v2enb1  29610  frgr3v  30360  extwwlkfab  30437  pjhthmo  31388  xrge0adddir  33093  archiabl  33274  dimvalfi  33761  pcmplfinf  34021  probun  34579  cnpconn  35428  satfv1lem  35560  outsideofeq  36328  linethru  36351  weiunso  36664  atlatmstc  39779  cvlcvr1  39799  ishlat3N  39814  hlrelat  39862  intnatN  39867  cvrval5  39875  atcvrlln  39980  llnexatN  39981  2at0mat0  39985  llncvrlpln  40018  lplnexllnN  40024  lplncvrlvol  40076  lncvrelatN  40241  pmapjoin  40312  pmapjat1  40313  pclclN  40351  osumclN  40427  lhprelat3N  40500  cdlemd5  40662  cdleme32fvcl  40900  cdlemg39  41176  ltrncom  41198  dihmeetALTN  41787  dochss  41825  mapdrvallem2  42105  nacsfix  43158  mzpsubst  43194  diophrw  43205  lzunuz  43214  jm2.19  43439  jm2.27  43454  hbtlem5  43574  tfsconcatrn  43788  nadd2rabtr  43830  fzunt  43900  iunrelexpuztr  44164  grumnudlem  44730  rfcnnnub  45485  3adantll2  45490  infleinf  45819  iccintsng  45971  mullimc  46064  mullimcf  46071  limcperiod  46076  cncfshift  46320  cncfperiod  46325  icccncfext  46333  stoweidlem20  46466  stoweidlem61  46507  fourierdlem73  46625  rmsupp0  48856  rmsuppss  48858  itschlc0xyqsol1  49254  itschlc0xyqsol  49255