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  7277  poxp3  8149  naddsuc2  8713  ordiso2  9529  iunfictbso  10128  fin1a2lem12  10425  fin1a2lem13  10426  prlem934  11047  ifle  13213  xlesubadd  13279  icoshftf1o  13491  elfzonelfzo  13785  fsuppmapnn0fiub0  14011  swrdcl  14663  repswccat  14804  subcn2  15611  rpdvds  16679  coprmprod  16680  qexpz  16921  ramval  17028  0ram  17040  cshwrepswhash1  17122  mreexexd  17660  gsmsymgreqlem1  19411  pmtrf  19436  odmulg  19537  pgpfi1  19576  lsmcl  21041  lbsextlem3  21121  islindf4  21798  coe1mul2  22206  cramerlem2  22626  cpmadugsumlemF  22814  cayhamlem4  22826  iscnp4  23201  cnpnei  23202  cnconst2  23221  cnpdis  23231  cnhaus  23292  ordthauslem  23321  clsconn  23368  nlly2i  23414  txcn  23564  ordthmeolem  23739  flimrest  23921  isfcf  23972  alexsubALTlem4  23988  ghmcnp  24053  utop2nei  24189  blssps  24363  blss  24364  metcnp3  24479  metcnp  24480  xrsxmet  24749  metdseq0  24794  xrhmeo  24895  cfil3i  25221  caucfil  25235  cfilres  25248  fta1b  26129  mumul  27143  lgsfcl2  27266  lgsdir  27295  lgsne0  27298  nolt02o  27659  nogt01o  27660  nosupbnd1lem3  27674  nosupbnd1lem4  27675  nosupbnd1lem5  27676  nosupbnd2  27680  noinfbnd1lem3  27689  noinfbnd1lem4  27690  noinfbnd1lem5  27691  noinfbnd2  27695  sleadd1  27948  sltmul2  28126  istrkgcb  28435  axbtwnid  28918  axcontlem2  28944  axcontlem4  28946  axcontlem7  28949  axcontlem8  28950  umgr2v2enb1  29506  frgr3v  30256  extwwlkfab  30333  pjhthmo  31283  xrge0adddir  33013  archiabl  33196  dimvalfi  33641  pcmplfinf  33892  probun  34451  cnpconn  35252  satfv1lem  35384  outsideofeq  36148  linethru  36171  weiunso  36484  atlatmstc  39337  cvlcvr1  39357  ishlat3N  39372  hlrelat  39421  intnatN  39426  cvrval5  39434  atcvrlln  39539  llnexatN  39540  2at0mat0  39544  llncvrlpln  39577  lplnexllnN  39583  lplncvrlvol  39635  lncvrelatN  39800  pmapjoin  39871  pmapjat1  39872  pclclN  39910  osumclN  39986  lhprelat3N  40059  cdlemd5  40221  cdleme32fvcl  40459  cdlemg39  40735  ltrncom  40757  dihmeetALTN  41346  dochss  41384  mapdrvallem2  41664  nacsfix  42735  mzpsubst  42771  diophrw  42782  lzunuz  42791  jm2.19  43017  jm2.27  43032  hbtlem5  43152  tfsconcatrn  43366  nadd2rabtr  43408  fzunt  43479  iunrelexpuztr  43743  grumnudlem  44309  rfcnnnub  45060  3adantll2  45065  infleinf  45399  iccintsng  45552  mullimc  45645  mullimcf  45652  limcperiod  45657  cncfshift  45903  cncfperiod  45908  icccncfext  45916  stoweidlem20  46049  stoweidlem61  46090  fourierdlem73  46208  rmsupp0  48343  rmsuppss  48345  itschlc0xyqsol1  48746  itschlc0xyqsol  48747