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  7230  poxp3  8092  naddsuc2  8629  ordiso2  9420  iunfictbso  10024  fin1a2lem12  10321  fin1a2lem13  10322  prlem934  10944  ifle  13112  xlesubadd  13178  icoshftf1o  13390  elfzonelfzo  13685  fsuppmapnn0fiub0  13916  swrdcl  14569  repswccat  14709  subcn2  15518  rpdvds  16587  coprmprod  16588  qexpz  16829  ramval  16936  0ram  16948  cshwrepswhash1  17030  mreexexd  17571  gsmsymgreqlem1  19359  pmtrf  19384  odmulg  19485  pgpfi1  19524  lsmcl  21035  lbsextlem3  21115  islindf4  21793  coe1mul2  22211  cramerlem2  22632  cpmadugsumlemF  22820  cayhamlem4  22832  iscnp4  23207  cnpnei  23208  cnconst2  23227  cnpdis  23237  cnhaus  23298  ordthauslem  23327  clsconn  23374  nlly2i  23420  txcn  23570  ordthmeolem  23745  flimrest  23927  isfcf  23978  alexsubALTlem4  23994  ghmcnp  24059  utop2nei  24194  blssps  24368  blss  24369  metcnp3  24484  metcnp  24485  xrsxmet  24754  metdseq0  24799  xrhmeo  24900  cfil3i  25225  caucfil  25239  cfilres  25252  fta1b  26133  mumul  27147  lgsfcl2  27270  lgsdir  27299  lgsne0  27302  nolt02o  27663  nogt01o  27664  nosupbnd1lem3  27678  nosupbnd1lem4  27679  nosupbnd1lem5  27680  nosupbnd2  27684  noinfbnd1lem3  27693  noinfbnd1lem4  27694  noinfbnd1lem5  27695  noinfbnd2  27699  leadds1  27985  ltmuls2  28167  istrkgcb  28528  axbtwnid  29012  axcontlem2  29038  axcontlem4  29040  axcontlem7  29043  axcontlem8  29044  umgr2v2enb1  29600  frgr3v  30350  extwwlkfab  30427  pjhthmo  31377  xrge0adddir  33100  archiabl  33280  dimvalfi  33758  pcmplfinf  34018  probun  34576  cnpconn  35424  satfv1lem  35556  outsideofeq  36324  linethru  36347  weiunso  36660  atlatmstc  39575  cvlcvr1  39595  ishlat3N  39610  hlrelat  39658  intnatN  39663  cvrval5  39671  atcvrlln  39776  llnexatN  39777  2at0mat0  39781  llncvrlpln  39814  lplnexllnN  39820  lplncvrlvol  39872  lncvrelatN  40037  pmapjoin  40108  pmapjat1  40109  pclclN  40147  osumclN  40223  lhprelat3N  40296  cdlemd5  40458  cdleme32fvcl  40696  cdlemg39  40972  ltrncom  40994  dihmeetALTN  41583  dochss  41621  mapdrvallem2  41901  nacsfix  42950  mzpsubst  42986  diophrw  42997  lzunuz  43006  jm2.19  43231  jm2.27  43246  hbtlem5  43366  tfsconcatrn  43580  nadd2rabtr  43622  fzunt  43692  iunrelexpuztr  43956  grumnudlem  44522  rfcnnnub  45277  3adantll2  45282  infleinf  45612  iccintsng  45765  mullimc  45858  mullimcf  45865  limcperiod  45870  cncfshift  46114  cncfperiod  46119  icccncfext  46127  stoweidlem20  46260  stoweidlem61  46301  fourierdlem73  46419  rmsupp0  48610  rmsuppss  48612  itschlc0xyqsol1  49008  itschlc0xyqsol  49009