Theorem simpll3 1210

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  f1prex  7040  ordiso2  8979  wemappo  9013  iunfictbso  9540  fin1a2lem12  9833  fin1a2lem13  9834  prlem934  10455  ifle  12591  xlesubadd  12657  icoshftf1o  12861  elfzonelfzo  13140  fsuppmapnn0fiub0  13362  swrdcl  14007  repswccat  14148  subcn2  14951  rpdvds  16004  coprmprod  16005  qexpz  16237  ramval  16344  0ram  16356  cshwrepswhash1  16436  mreexexd  16919  gsumccatOLD  18005  gsmsymgreqlem1  18558  pmtrf  18583  odmulg  18683  pgpfi1  18720  lsmcl  19855  lbsextlem3  19932  coe1mul2  20437  islindf4  20982  cramerlem2  21297  cpmadugsumlemF  21484  cayhamlem4  21496  iscnp4  21871  cnpnei  21872  cnconst2  21891  cnpdis  21901  cnhaus  21962  ordthauslem  21991  clsconn  22038  nlly2i  22084  txcn  22234  ordthmeolem  22409  flimrest  22591  isfcf  22642  alexsubALTlem4  22658  ghmcnp  22723  utop2nei  22859  blssps  23034  blss  23035  metcnp3  23150  metcnp  23151  xrsxmet  23417  metdseq0  23462  xrhmeo  23550  cfil3i  23872  caucfil  23886  cfilres  23899  fta1b  24763  mumul  25758  lgsfcl2  25879  lgsdir  25908  lgsne0  25911  istrkgcb  26242  axbtwnid  26725  axcontlem2  26751  axcontlem4  26753  axcontlem7  26756  axcontlem8  26757  umgr2v2enb1  27308  frgr3v  28054  extwwlkfab  28131  pjhthmo  29079  xrge0adddir  30679  archiabl  30827  dimvalfi  31002  pcmplfinf  31125  probun  31677  cnpconn  32477  satfv1lem  32609  nolt02o  33199  nosupbnd1lem3  33210  nosupbnd1lem4  33211  nosupbnd1lem5  33212  nosupbnd2  33216  outsideofeq  33591  linethru  33614  atlatmstc  36470  cvlcvr1  36490  ishlat3N  36505  hlrelat  36553  intnatN  36558  cvrval5  36566  atcvrlln  36671  llnexatN  36672  2at0mat0  36676  llncvrlpln  36709  lplnexllnN  36715  lplncvrlvol  36767  lncvrelatN  36932  pmapjoin  37003  pmapjat1  37004  pclclN  37042  osumclN  37118  lhprelat3N  37191  cdlemd5  37353  cdleme32fvcl  37591  cdlemg39  37867  ltrncom  37889  dihmeetALTN  38478  dochss  38516  mapdrvallem2  38796  nacsfix  39329  mzpsubst  39365  diophrw  39376  lzunuz  39385  jm2.19  39610  jm2.27  39625  hbtlem5  39748  iunrelexpuztr  40084  grumnudlem  40641  rfcnnnub  41313  3adantll2  41320  infleinf  41660  iccintsng  41819  mullimc  41917  mullimcf  41924  limcperiod  41929  cncfshift  42177  cncfperiod  42182  icccncfext  42190  stoweidlem20  42325  stoweidlem61  42366  fourierdlem73  42484  rmsupp0  44436  rmsuppss  44438  itschlc0xyqsol1  44773  itschlc0xyqsol  44774