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  7225  poxp3  8090  naddsuc2  8626  ordiso2  9426  iunfictbso  10027  fin1a2lem12  10324  fin1a2lem13  10325  prlem934  10946  ifle  13117  xlesubadd  13183  icoshftf1o  13395  elfzonelfzo  13690  fsuppmapnn0fiub0  13918  swrdcl  14570  repswccat  14710  subcn2  15520  rpdvds  16589  coprmprod  16590  qexpz  16831  ramval  16938  0ram  16950  cshwrepswhash1  17032  mreexexd  17572  gsmsymgreqlem1  19327  pmtrf  19352  odmulg  19453  pgpfi1  19492  lsmcl  21005  lbsextlem3  21085  islindf4  21763  coe1mul2  22171  cramerlem2  22591  cpmadugsumlemF  22779  cayhamlem4  22791  iscnp4  23166  cnpnei  23167  cnconst2  23186  cnpdis  23196  cnhaus  23257  ordthauslem  23286  clsconn  23333  nlly2i  23379  txcn  23529  ordthmeolem  23704  flimrest  23886  isfcf  23937  alexsubALTlem4  23953  ghmcnp  24018  utop2nei  24154  blssps  24328  blss  24329  metcnp3  24444  metcnp  24445  xrsxmet  24714  metdseq0  24759  xrhmeo  24860  cfil3i  25185  caucfil  25199  cfilres  25212  fta1b  26093  mumul  27107  lgsfcl2  27230  lgsdir  27259  lgsne0  27262  nolt02o  27623  nogt01o  27624  nosupbnd1lem3  27638  nosupbnd1lem4  27639  nosupbnd1lem5  27640  nosupbnd2  27644  noinfbnd1lem3  27653  noinfbnd1lem4  27654  noinfbnd1lem5  27655  noinfbnd2  27659  sleadd1  27919  sltmul2  28097  istrkgcb  28419  axbtwnid  28902  axcontlem2  28928  axcontlem4  28930  axcontlem7  28933  axcontlem8  28934  umgr2v2enb1  29490  frgr3v  30237  extwwlkfab  30314  pjhthmo  31264  xrge0adddir  32985  archiabl  33153  dimvalfi  33576  pcmplfinf  33830  probun  34389  cnpconn  35205  satfv1lem  35337  outsideofeq  36106  linethru  36129  weiunso  36442  atlatmstc  39300  cvlcvr1  39320  ishlat3N  39335  hlrelat  39384  intnatN  39389  cvrval5  39397  atcvrlln  39502  llnexatN  39503  2at0mat0  39507  llncvrlpln  39540  lplnexllnN  39546  lplncvrlvol  39598  lncvrelatN  39763  pmapjoin  39834  pmapjat1  39835  pclclN  39873  osumclN  39949  lhprelat3N  40022  cdlemd5  40184  cdleme32fvcl  40422  cdlemg39  40698  ltrncom  40720  dihmeetALTN  41309  dochss  41347  mapdrvallem2  41627  nacsfix  42688  mzpsubst  42724  diophrw  42735  lzunuz  42744  jm2.19  42969  jm2.27  42984  hbtlem5  43104  tfsconcatrn  43318  nadd2rabtr  43360  fzunt  43431  iunrelexpuztr  43695  grumnudlem  44261  rfcnnnub  45017  3adantll2  45022  infleinf  45355  iccintsng  45508  mullimc  45601  mullimcf  45608  limcperiod  45613  cncfshift  45859  cncfperiod  45864  icccncfext  45872  stoweidlem20  46005  stoweidlem61  46046  fourierdlem73  46164  rmsupp0  48356  rmsuppss  48358  itschlc0xyqsol1  48755  itschlc0xyqsol  48756