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  7293  poxp3  8155  naddsuc2  8697  ordiso2  9487  iunfictbso  10117  fin1a2lem12  10413  fin1a2lem13  10414  prlem934  11036  ifle  13241  xlesubadd  13307  icoshftf1o  13519  elfzonelfzo  13817  fsuppmapnn0fiub0  14049  swrdcl  14705  repswccat  14849  subcn2  15672  rpdvds  16743  coprmprod  16744  qexpz  16986  ramval  17093  0ram  17105  cshwrepswhash1  17187  mreexexd  17729  gsmsymgreqlem1  19531  pmtrf  19556  odmulg  19657  pgpfi1  19696  lsmcl  21241  lbsextlem3  21321  islindf4  22025  coe1mul2  22467  cramerlem2  22882  cpmadugsumlemF  23070  cayhamlem4  23082  iscnp4  23457  cnpnei  23458  cnconst2  23477  cnpdis  23487  cnhaus  23548  ordthauslem  23577  clsconn  23624  nlly2i  23670  txcn  23820  ordthmeolem  23995  flimrest  24177  isfcf  24228  alexsubALTlem4  24244  ghmcnp  24309  utop2nei  24444  blssps  24618  blss  24619  metcnp3  24734  metcnp  24735  xrsxmet  25004  metdseq0  25049  xrhmeo  25142  cfil3i  25465  caucfil  25479  cfilres  25492  fta1b  26366  mumul  27382  lgsfcl2  27504  lgsdir  27533  lgsne0  27536  nolt02o  27896  nogt01o  27897  nosupbnd1lem3  27911  nosupbnd1lem4  27912  nosupbnd1lem5  27913  nosupbnd2  27917  noinfbnd1lem3  27926  noinfbnd1lem4  27927  noinfbnd1lem5  27928  noinfbnd2  27932  leadds1  28219  ltmuls2  28401  istrkgcb  28762  axbtwnid  29326  axcontlem2  29352  axcontlem4  29354  axcontlem7  29357  axcontlem8  29358  umgr2v2enb1  29913  frgr3v  30663  extwwlkfab  30740  pjhthmo  31691  xrge0adddir  33369  archiabl  33549  dimvalfi  34023  pcmplfinf  34282  probun  34841  cnpconn  35743  satfv1lem  35875  outsideofeq  36643  linethru  36666  weiunso  37018  atlatmstc  40134  cvlcvr1  40154  ishlat3N  40169  hlrelat  40217  intnatN  40222  cvrval5  40230  atcvrlln  40335  llnexatN  40336  2at0mat0  40340  llncvrlpln  40373  lplnexllnN  40379  lplncvrlvol  40431  lncvrelatN  40596  pmapjoin  40667  pmapjat1  40668  pclclN  40706  osumclN  40782  lhprelat3N  40855  cdlemd5  41017  cdleme32fvcl  41255  cdlemg39  41531  ltrncom  41553  dihmeetALTN  42142  dochss  42180  mapdrvallem2  42460  nacsfix  43484  mzpsubst  43520  diophrw  43531  lzunuz  43540  jm2.19  43761  jm2.27  43776  hbtlem5  43896  tfsconcatrn  44110  nadd2rabtr  44152  fzunt  44222  iunrelexpuztr  44486  grumnudlem  45036  rfcnnnub  45797  3adantll2  45802  infleinf  46128  iccintsng  46280  mullimc  46373  mullimcf  46380  limcperiod  46385  cncfshift  46629  cncfperiod  46634  icccncfext  46642  stoweidlem20  46775  stoweidlem61  46816  fourierdlem73  46934  rmsupp0  49189  rmsuppss  49191  itschlc0xyqsol1  49587  itschlc0xyqsol  49588