Theorem simpll3 1213

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  f1prex  7156  ordiso2  9274  iunfictbso  9870  fin1a2lem12  10167  fin1a2lem13  10168  prlem934  10789  ifle  12931  xlesubadd  12997  icoshftf1o  13206  elfzonelfzo  13489  fsuppmapnn0fiub0  13713  swrdcl  14358  repswccat  14499  subcn2  15304  rpdvds  16365  coprmprod  16366  qexpz  16602  ramval  16709  0ram  16721  cshwrepswhash1  16804  mreexexd  17357  gsumccatOLD  18479  gsmsymgreqlem1  19038  pmtrf  19063  odmulg  19163  pgpfi1  19200  lsmcl  20345  lbsextlem3  20422  islindf4  21045  coe1mul2  21440  cramerlem2  21837  cpmadugsumlemF  22025  cayhamlem4  22037  iscnp4  22414  cnpnei  22415  cnconst2  22434  cnpdis  22444  cnhaus  22505  ordthauslem  22534  clsconn  22581  nlly2i  22627  txcn  22777  ordthmeolem  22952  flimrest  23134  isfcf  23185  alexsubALTlem4  23201  ghmcnp  23266  utop2nei  23402  blssps  23577  blss  23578  metcnp3  23696  metcnp  23697  xrsxmet  23972  metdseq0  24017  xrhmeo  24109  cfil3i  24433  caucfil  24447  cfilres  24460  fta1b  25334  mumul  26330  lgsfcl2  26451  lgsdir  26480  lgsne0  26483  istrkgcb  26817  axbtwnid  27307  axcontlem2  27333  axcontlem4  27335  axcontlem7  27338  axcontlem8  27339  umgr2v2enb1  27893  frgr3v  28639  extwwlkfab  28716  pjhthmo  29664  xrge0adddir  31301  archiabl  31452  dimvalfi  31687  pcmplfinf  31811  probun  32386  cnpconn  33192  satfv1lem  33324  nolt02o  33898  nogt01o  33899  nosupbnd1lem3  33913  nosupbnd1lem4  33914  nosupbnd1lem5  33915  nosupbnd2  33919  noinfbnd1lem3  33928  noinfbnd1lem4  33929  noinfbnd1lem5  33930  noinfbnd2  33934  outsideofeq  34432  linethru  34455  atlatmstc  37333  cvlcvr1  37353  ishlat3N  37368  hlrelat  37416  intnatN  37421  cvrval5  37429  atcvrlln  37534  llnexatN  37535  2at0mat0  37539  llncvrlpln  37572  lplnexllnN  37578  lplncvrlvol  37630  lncvrelatN  37795  pmapjoin  37866  pmapjat1  37867  pclclN  37905  osumclN  37981  lhprelat3N  38054  cdlemd5  38216  cdleme32fvcl  38454  cdlemg39  38730  ltrncom  38752  dihmeetALTN  39341  dochss  39379  mapdrvallem2  39659  nacsfix  40534  mzpsubst  40570  diophrw  40581  lzunuz  40590  jm2.19  40815  jm2.27  40830  hbtlem5  40953  fzunt  41062  iunrelexpuztr  41327  grumnudlem  41903  rfcnnnub  42579  3adantll2  42586  infleinf  42911  iccintsng  43061  mullimc  43157  mullimcf  43164  limcperiod  43169  cncfshift  43415  cncfperiod  43420  icccncfext  43428  stoweidlem20  43561  stoweidlem61  43602  fourierdlem73  43720  rmsupp0  45704  rmsuppss  45706  itschlc0xyqsol1  46112  itschlc0xyqsol  46113