Theorem simpll3 1215

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 726	1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1088

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 400  df-3an 1090

This theorem is referenced by:  f1prex  7063  ordiso2  9064  iunfictbso  9626  fin1a2lem12  9923  fin1a2lem13  9924  prlem934  10545  ifle  12685  xlesubadd  12751  icoshftf1o  12960  elfzonelfzo  13242  fsuppmapnn0fiub0  13464  swrdcl  14108  repswccat  14249  subcn2  15054  rpdvds  16113  coprmprod  16114  qexpz  16349  ramval  16456  0ram  16468  cshwrepswhash1  16551  mreexexd  17034  gsumccatOLD  18133  gsmsymgreqlem1  18688  pmtrf  18713  odmulg  18813  pgpfi1  18850  lsmcl  19986  lbsextlem3  20063  islindf4  20666  coe1mul2  21056  cramerlem2  21451  cpmadugsumlemF  21639  cayhamlem4  21651  iscnp4  22026  cnpnei  22027  cnconst2  22046  cnpdis  22056  cnhaus  22117  ordthauslem  22146  clsconn  22193  nlly2i  22239  txcn  22389  ordthmeolem  22564  flimrest  22746  isfcf  22797  alexsubALTlem4  22813  ghmcnp  22878  utop2nei  23014  blssps  23189  blss  23190  metcnp3  23305  metcnp  23306  xrsxmet  23573  metdseq0  23618  xrhmeo  23710  cfil3i  24033  caucfil  24047  cfilres  24060  fta1b  24934  mumul  25930  lgsfcl2  26051  lgsdir  26080  lgsne0  26083  istrkgcb  26414  axbtwnid  26897  axcontlem2  26923  axcontlem4  26925  axcontlem7  26928  axcontlem8  26929  umgr2v2enb1  27480  frgr3v  28224  extwwlkfab  28301  pjhthmo  29249  xrge0adddir  30890  archiabl  31041  dimvalfi  31271  pcmplfinf  31395  probun  31968  cnpconn  32775  satfv1lem  32907  nolt02o  33553  nogt01o  33554  nosupbnd1lem3  33568  nosupbnd1lem4  33569  nosupbnd1lem5  33570  nosupbnd2  33574  noinfbnd1lem3  33583  noinfbnd1lem4  33584  noinfbnd1lem5  33585  noinfbnd2  33589  outsideofeq  34087  linethru  34110  atlatmstc  36988  cvlcvr1  37008  ishlat3N  37023  hlrelat  37071  intnatN  37076  cvrval5  37084  atcvrlln  37189  llnexatN  37190  2at0mat0  37194  llncvrlpln  37227  lplnexllnN  37233  lplncvrlvol  37285  lncvrelatN  37450  pmapjoin  37521  pmapjat1  37522  pclclN  37560  osumclN  37636  lhprelat3N  37709  cdlemd5  37871  cdleme32fvcl  38109  cdlemg39  38385  ltrncom  38407  dihmeetALTN  38996  dochss  39034  mapdrvallem2  39314  nacsfix  40146  mzpsubst  40182  diophrw  40193  lzunuz  40202  jm2.19  40427  jm2.27  40442  hbtlem5  40565  iunrelexpuztr  40913  grumnudlem  41485  rfcnnnub  42157  3adantll2  42164  infleinf  42489  iccintsng  42641  mullimc  42739  mullimcf  42746  limcperiod  42751  cncfshift  42997  cncfperiod  43002  icccncfext  43010  stoweidlem20  43143  stoweidlem61  43184  fourierdlem73  43302  rmsupp0  45285  rmsuppss  45287  itschlc0xyqsol1  45693  itschlc0xyqsol  45694