Theorem simpll3 1210

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  f1prex  7034  ordiso2  8973  wemappo  9007  iunfictbso  9534  fin1a2lem12  9827  fin1a2lem13  9828  prlem934  10449  ifle  12584  xlesubadd  12650  icoshftf1o  12854  elfzonelfzo  13133  fsuppmapnn0fiub0  13355  swrdcl  14001  repswccat  14142  subcn2  14945  rpdvds  15998  coprmprod  15999  qexpz  16231  ramval  16338  0ram  16350  cshwrepswhash1  16430  mreexexd  16913  gsumccatOLD  17999  gsmsymgreqlem1  18552  pmtrf  18577  odmulg  18677  pgpfi1  18714  lsmcl  19849  lbsextlem3  19926  coe1mul2  20431  islindf4  20976  cramerlem2  21291  cpmadugsumlemF  21478  cayhamlem4  21490  iscnp4  21865  cnpnei  21866  cnconst2  21885  cnpdis  21895  cnhaus  21956  ordthauslem  21985  clsconn  22032  nlly2i  22078  txcn  22228  ordthmeolem  22403  flimrest  22585  isfcf  22636  alexsubALTlem4  22652  ghmcnp  22717  utop2nei  22853  blssps  23028  blss  23029  metcnp3  23144  metcnp  23145  xrsxmet  23411  metdseq0  23456  xrhmeo  23544  cfil3i  23866  caucfil  23880  cfilres  23893  fta1b  24757  mumul  25752  lgsfcl2  25873  lgsdir  25902  lgsne0  25905  istrkgcb  26236  axbtwnid  26719  axcontlem2  26745  axcontlem4  26747  axcontlem7  26750  axcontlem8  26751  umgr2v2enb1  27302  frgr3v  28048  extwwlkfab  28125  pjhthmo  29073  xrge0adddir  30674  archiabl  30822  dimvalfi  30997  pcmplfinf  31120  probun  31672  cnpconn  32472  satfv1lem  32604  nolt02o  33194  nosupbnd1lem3  33205  nosupbnd1lem4  33206  nosupbnd1lem5  33207  nosupbnd2  33211  outsideofeq  33586  linethru  33609  atlatmstc  36449  cvlcvr1  36469  ishlat3N  36484  hlrelat  36532  intnatN  36537  cvrval5  36545  atcvrlln  36650  llnexatN  36651  2at0mat0  36655  llncvrlpln  36688  lplnexllnN  36694  lplncvrlvol  36746  lncvrelatN  36911  pmapjoin  36982  pmapjat1  36983  pclclN  37021  osumclN  37097  lhprelat3N  37170  cdlemd5  37332  cdleme32fvcl  37570  cdlemg39  37846  ltrncom  37868  dihmeetALTN  38457  dochss  38495  mapdrvallem2  38775  nacsfix  39302  mzpsubst  39338  diophrw  39349  lzunuz  39358  jm2.19  39583  jm2.27  39598  hbtlem5  39721  iunrelexpuztr  40057  grumnudlem  40614  rfcnnnub  41286  3adantll2  41293  infleinf  41633  iccintsng  41792  mullimc  41890  mullimcf  41897  limcperiod  41902  cncfshift  42150  cncfperiod  42155  icccncfext  42163  stoweidlem20  42299  stoweidlem61  42340  fourierdlem73  42458  rmsupp0  44410  rmsuppss  44412  itschlc0xyqsol1  44747  itschlc0xyqsol  44748