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  7218  poxp3  8080  naddsuc2  8616  ordiso2  9401  iunfictbso  10005  fin1a2lem12  10302  fin1a2lem13  10303  prlem934  10924  ifle  13096  xlesubadd  13162  icoshftf1o  13374  elfzonelfzo  13669  fsuppmapnn0fiub0  13900  swrdcl  14553  repswccat  14693  subcn2  15502  rpdvds  16571  coprmprod  16572  qexpz  16813  ramval  16920  0ram  16932  cshwrepswhash1  17014  mreexexd  17554  gsmsymgreqlem1  19343  pmtrf  19368  odmulg  19469  pgpfi1  19508  lsmcl  21018  lbsextlem3  21098  islindf4  21776  coe1mul2  22184  cramerlem2  22604  cpmadugsumlemF  22792  cayhamlem4  22804  iscnp4  23179  cnpnei  23180  cnconst2  23199  cnpdis  23209  cnhaus  23270  ordthauslem  23299  clsconn  23346  nlly2i  23392  txcn  23542  ordthmeolem  23717  flimrest  23899  isfcf  23950  alexsubALTlem4  23966  ghmcnp  24031  utop2nei  24166  blssps  24340  blss  24341  metcnp3  24456  metcnp  24457  xrsxmet  24726  metdseq0  24771  xrhmeo  24872  cfil3i  25197  caucfil  25211  cfilres  25224  fta1b  26105  mumul  27119  lgsfcl2  27242  lgsdir  27271  lgsne0  27274  nolt02o  27635  nogt01o  27636  nosupbnd1lem3  27650  nosupbnd1lem4  27651  nosupbnd1lem5  27652  nosupbnd2  27656  noinfbnd1lem3  27665  noinfbnd1lem4  27666  noinfbnd1lem5  27667  noinfbnd2  27671  sleadd1  27933  sltmul2  28111  istrkgcb  28435  axbtwnid  28918  axcontlem2  28944  axcontlem4  28946  axcontlem7  28949  axcontlem8  28950  umgr2v2enb1  29506  frgr3v  30253  extwwlkfab  30330  pjhthmo  31280  xrge0adddir  32997  archiabl  33165  dimvalfi  33612  pcmplfinf  33872  probun  34430  cnpconn  35272  satfv1lem  35404  outsideofeq  36170  linethru  36193  weiunso  36506  atlatmstc  39364  cvlcvr1  39384  ishlat3N  39399  hlrelat  39447  intnatN  39452  cvrval5  39460  atcvrlln  39565  llnexatN  39566  2at0mat0  39570  llncvrlpln  39603  lplnexllnN  39609  lplncvrlvol  39661  lncvrelatN  39826  pmapjoin  39897  pmapjat1  39898  pclclN  39936  osumclN  40012  lhprelat3N  40085  cdlemd5  40247  cdleme32fvcl  40485  cdlemg39  40761  ltrncom  40783  dihmeetALTN  41372  dochss  41410  mapdrvallem2  41690  nacsfix  42751  mzpsubst  42787  diophrw  42798  lzunuz  42807  jm2.19  43032  jm2.27  43047  hbtlem5  43167  tfsconcatrn  43381  nadd2rabtr  43423  fzunt  43494  iunrelexpuztr  43758  grumnudlem  44324  rfcnnnub  45079  3adantll2  45084  infleinf  45416  iccintsng  45569  mullimc  45662  mullimcf  45669  limcperiod  45674  cncfshift  45918  cncfperiod  45923  icccncfext  45931  stoweidlem20  46064  stoweidlem61  46105  fourierdlem73  46223  rmsupp0  48405  rmsuppss  48407  itschlc0xyqsol1  48804  itschlc0xyqsol  48805