Theorem simpll3 1211

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1084

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 396  df-3an 1086

This theorem is referenced by:  f1prex  7274  poxp3  8130  ordiso2  9506  iunfictbso  10105  fin1a2lem12  10402  fin1a2lem13  10403  prlem934  11024  ifle  13173  xlesubadd  13239  icoshftf1o  13448  elfzonelfzo  13731  fsuppmapnn0fiub0  13955  swrdcl  14592  repswccat  14733  subcn2  15536  rpdvds  16594  coprmprod  16595  qexpz  16833  ramval  16940  0ram  16952  cshwrepswhash1  17035  mreexexd  17591  gsmsymgreqlem1  19340  pmtrf  19365  odmulg  19466  pgpfi1  19505  lsmcl  20921  lbsextlem3  21001  islindf4  21701  coe1mul2  22110  cramerlem2  22512  cpmadugsumlemF  22700  cayhamlem4  22712  iscnp4  23089  cnpnei  23090  cnconst2  23109  cnpdis  23119  cnhaus  23180  ordthauslem  23209  clsconn  23256  nlly2i  23302  txcn  23452  ordthmeolem  23627  flimrest  23809  isfcf  23860  alexsubALTlem4  23876  ghmcnp  23941  utop2nei  24077  blssps  24252  blss  24253  metcnp3  24371  metcnp  24372  xrsxmet  24647  metdseq0  24692  xrhmeo  24793  cfil3i  25119  caucfil  25133  cfilres  25146  fta1b  26027  mumul  27029  lgsfcl2  27152  lgsdir  27181  lgsne0  27184  nolt02o  27544  nogt01o  27545  nosupbnd1lem3  27559  nosupbnd1lem4  27560  nosupbnd1lem5  27561  nosupbnd2  27565  noinfbnd1lem3  27574  noinfbnd1lem4  27575  noinfbnd1lem5  27576  noinfbnd2  27580  sleadd1  27822  sltmul2  27987  istrkgcb  28176  axbtwnid  28666  axcontlem2  28692  axcontlem4  28694  axcontlem7  28697  axcontlem8  28698  umgr2v2enb1  29252  frgr3v  29997  extwwlkfab  30074  pjhthmo  31024  xrge0adddir  32658  archiabl  32812  dimvalfi  33165  pcmplfinf  33330  probun  33907  cnpconn  34710  satfv1lem  34842  outsideofeq  35597  linethru  35620  atlatmstc  38679  cvlcvr1  38699  ishlat3N  38714  hlrelat  38763  intnatN  38768  cvrval5  38776  atcvrlln  38881  llnexatN  38882  2at0mat0  38886  llncvrlpln  38919  lplnexllnN  38925  lplncvrlvol  38977  lncvrelatN  39142  pmapjoin  39213  pmapjat1  39214  pclclN  39252  osumclN  39328  lhprelat3N  39401  cdlemd5  39563  cdleme32fvcl  39801  cdlemg39  40077  ltrncom  40099  dihmeetALTN  40688  dochss  40726  mapdrvallem2  41006  nacsfix  41939  mzpsubst  41975  diophrw  41986  lzunuz  41995  jm2.19  42221  jm2.27  42236  hbtlem5  42359  tfsconcatrn  42581  nadd2rabtr  42623  naddsuc2  42632  fzunt  42695  iunrelexpuztr  42959  grumnudlem  43533  rfcnnnub  44209  3adantll2  44214  infleinf  44567  iccintsng  44721  mullimc  44817  mullimcf  44824  limcperiod  44829  cncfshift  45075  cncfperiod  45080  icccncfext  45088  stoweidlem20  45221  stoweidlem61  45262  fourierdlem73  45380  rmsupp0  47233  rmsuppss  47235  itschlc0xyqsol1  47640  itschlc0xyqsol  47641