Theorem simpll3 1221

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  f1prex  7235  poxp3  8097  naddsuc2  8634  ordiso2  9427  iunfictbso  10034  fin1a2lem12  10331  fin1a2lem13  10332  prlem934  10954  ifle  13147  xlesubadd  13213  icoshftf1o  13425  elfzonelfzo  13722  fsuppmapnn0fiub0  13953  swrdcl  14606  repswccat  14746  subcn2  15555  rpdvds  16627  coprmprod  16628  qexpz  16870  ramval  16977  0ram  16989  cshwrepswhash1  17071  mreexexd  17612  gsmsymgreqlem1  19403  pmtrf  19428  odmulg  19529  pgpfi1  19568  lsmcl  21080  lbsextlem3  21160  islindf4  21820  coe1mul2  22262  cramerlem2  22678  cpmadugsumlemF  22866  cayhamlem4  22878  iscnp4  23253  cnpnei  23254  cnconst2  23273  cnpdis  23283  cnhaus  23344  ordthauslem  23373  clsconn  23420  nlly2i  23466  txcn  23616  ordthmeolem  23791  flimrest  23973  isfcf  24024  alexsubALTlem4  24040  ghmcnp  24105  utop2nei  24240  blssps  24414  blss  24415  metcnp3  24530  metcnp  24531  xrsxmet  24800  metdseq0  24845  xrhmeo  24938  cfil3i  25261  caucfil  25275  cfilres  25288  fta1b  26162  mumul  27169  lgsfcl2  27291  lgsdir  27320  lgsne0  27323  nolt02o  27684  nogt01o  27685  nosupbnd1lem3  27699  nosupbnd1lem4  27700  nosupbnd1lem5  27701  nosupbnd2  27705  noinfbnd1lem3  27714  noinfbnd1lem4  27715  noinfbnd1lem5  27716  noinfbnd2  27720  leadds1  28006  ltmuls2  28188  istrkgcb  28549  axbtwnid  29033  axcontlem2  29059  axcontlem4  29061  axcontlem7  29064  axcontlem8  29065  umgr2v2enb1  29620  frgr3v  30370  extwwlkfab  30447  pjhthmo  31398  xrge0adddir  33104  archiabl  33286  dimvalfi  33793  pcmplfinf  34052  probun  34610  cnpconn  35465  satfv1lem  35597  outsideofeq  36365  linethru  36388  weiunso  36701  atlatmstc  39818  cvlcvr1  39838  ishlat3N  39853  hlrelat  39901  intnatN  39906  cvrval5  39914  atcvrlln  40019  llnexatN  40020  2at0mat0  40024  llncvrlpln  40057  lplnexllnN  40063  lplncvrlvol  40115  lncvrelatN  40280  pmapjoin  40351  pmapjat1  40352  pclclN  40390  osumclN  40466  lhprelat3N  40539  cdlemd5  40701  cdleme32fvcl  40939  cdlemg39  41215  ltrncom  41237  dihmeetALTN  41826  dochss  41864  mapdrvallem2  42144  nacsfix  43168  mzpsubst  43204  diophrw  43215  lzunuz  43224  jm2.19  43445  jm2.27  43460  hbtlem5  43580  tfsconcatrn  43794  nadd2rabtr  43836  fzunt  43906  iunrelexpuztr  44170  grumnudlem  44736  rfcnnnub  45491  3adantll2  45496  infleinf  45823  iccintsng  45975  mullimc  46068  mullimcf  46075  limcperiod  46080  cncfshift  46324  cncfperiod  46329  icccncfext  46337  stoweidlem20  46470  stoweidlem61  46511  fourierdlem73  46629  rmsupp0  48866  rmsuppss  48868  itschlc0xyqsol1  49264  itschlc0xyqsol  49265