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

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

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

This theorem is referenced by:  f1prex  7262  poxp3  8132  naddsuc2  8668  ordiso2  9475  iunfictbso  10074  fin1a2lem12  10371  fin1a2lem13  10372  prlem934  10993  ifle  13164  xlesubadd  13230  icoshftf1o  13442  elfzonelfzo  13737  fsuppmapnn0fiub0  13965  swrdcl  14617  repswccat  14758  subcn2  15568  rpdvds  16637  coprmprod  16638  qexpz  16879  ramval  16986  0ram  16998  cshwrepswhash1  17080  mreexexd  17616  gsmsymgreqlem1  19367  pmtrf  19392  odmulg  19493  pgpfi1  19532  lsmcl  20997  lbsextlem3  21077  islindf4  21754  coe1mul2  22162  cramerlem2  22582  cpmadugsumlemF  22770  cayhamlem4  22782  iscnp4  23157  cnpnei  23158  cnconst2  23177  cnpdis  23187  cnhaus  23248  ordthauslem  23277  clsconn  23324  nlly2i  23370  txcn  23520  ordthmeolem  23695  flimrest  23877  isfcf  23928  alexsubALTlem4  23944  ghmcnp  24009  utop2nei  24145  blssps  24319  blss  24320  metcnp3  24435  metcnp  24436  xrsxmet  24705  metdseq0  24750  xrhmeo  24851  cfil3i  25176  caucfil  25190  cfilres  25203  fta1b  26084  mumul  27098  lgsfcl2  27221  lgsdir  27250  lgsne0  27253  nolt02o  27614  nogt01o  27615  nosupbnd1lem3  27629  nosupbnd1lem4  27630  nosupbnd1lem5  27631  nosupbnd2  27635  noinfbnd1lem3  27644  noinfbnd1lem4  27645  noinfbnd1lem5  27646  noinfbnd2  27650  sleadd1  27903  sltmul2  28081  istrkgcb  28390  axbtwnid  28873  axcontlem2  28899  axcontlem4  28901  axcontlem7  28904  axcontlem8  28905  umgr2v2enb1  29461  frgr3v  30211  extwwlkfab  30288  pjhthmo  31238  xrge0adddir  32966  archiabl  33159  dimvalfi  33604  pcmplfinf  33858  probun  34417  cnpconn  35224  satfv1lem  35356  outsideofeq  36125  linethru  36148  weiunso  36461  atlatmstc  39319  cvlcvr1  39339  ishlat3N  39354  hlrelat  39403  intnatN  39408  cvrval5  39416  atcvrlln  39521  llnexatN  39522  2at0mat0  39526  llncvrlpln  39559  lplnexllnN  39565  lplncvrlvol  39617  lncvrelatN  39782  pmapjoin  39853  pmapjat1  39854  pclclN  39892  osumclN  39968  lhprelat3N  40041  cdlemd5  40203  cdleme32fvcl  40441  cdlemg39  40717  ltrncom  40739  dihmeetALTN  41328  dochss  41366  mapdrvallem2  41646  nacsfix  42707  mzpsubst  42743  diophrw  42754  lzunuz  42763  jm2.19  42989  jm2.27  43004  hbtlem5  43124  tfsconcatrn  43338  nadd2rabtr  43380  fzunt  43451  iunrelexpuztr  43715  grumnudlem  44281  rfcnnnub  45037  3adantll2  45042  infleinf  45375  iccintsng  45528  mullimc  45621  mullimcf  45628  limcperiod  45633  cncfshift  45879  cncfperiod  45884  icccncfext  45892  stoweidlem20  46025  stoweidlem61  46066  fourierdlem73  46184  rmsupp0  48360  rmsuppss  48362  itschlc0xyqsol1  48759  itschlc0xyqsol  48760