Theorem simpll3 1233

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  f1prex  7284  poxp3  8147  naddsuc2  8689  ordiso2  9478  iunfictbso  10099  fin1a2lem12  10396  fin1a2lem13  10397  prlem934  11019  ifle  13224  xlesubadd  13290  icoshftf1o  13502  elfzonelfzo  13800  fsuppmapnn0fiub0  14031  swrdcl  14685  repswccat  14825  subcn2  15648  rpdvds  16719  coprmprod  16720  qexpz  16962  ramval  17069  0ram  17081  cshwrepswhash1  17163  mreexexd  17705  gsmsymgreqlem1  19501  pmtrf  19526  odmulg  19627  pgpfi1  19666  lsmcl  21185  lbsextlem3  21265  islindf4  21969  coe1mul2  22411  cramerlem2  22826  cpmadugsumlemF  23014  cayhamlem4  23026  iscnp4  23401  cnpnei  23402  cnconst2  23421  cnpdis  23431  cnhaus  23492  ordthauslem  23521  clsconn  23568  nlly2i  23614  txcn  23764  ordthmeolem  23939  flimrest  24121  isfcf  24172  alexsubALTlem4  24188  ghmcnp  24253  utop2nei  24388  blssps  24562  blss  24563  metcnp3  24678  metcnp  24679  xrsxmet  24948  metdseq0  24993  xrhmeo  25086  cfil3i  25409  caucfil  25423  cfilres  25436  fta1b  26310  mumul  27326  lgsfcl2  27448  lgsdir  27477  lgsne0  27480  nolt02o  27840  nogt01o  27841  nosupbnd1lem3  27855  nosupbnd1lem4  27856  nosupbnd1lem5  27857  nosupbnd2  27861  noinfbnd1lem3  27870  noinfbnd1lem4  27871  noinfbnd1lem5  27872  noinfbnd2  27876  leadds1  28163  ltmuls2  28345  istrkgcb  28706  axbtwnid  29270  axcontlem2  29296  axcontlem4  29298  axcontlem7  29301  axcontlem8  29302  umgr2v2enb1  29857  frgr3v  30607  extwwlkfab  30684  pjhthmo  31635  xrge0adddir  33319  archiabl  33499  dimvalfi  33973  pcmplfinf  34232  probun  34790  cnpconn  35703  satfv1lem  35835  outsideofeq  36603  linethru  36626  weiunso  36958  atlatmstc  40074  cvlcvr1  40094  ishlat3N  40109  hlrelat  40157  intnatN  40162  cvrval5  40170  atcvrlln  40275  llnexatN  40276  2at0mat0  40280  llncvrlpln  40313  lplnexllnN  40319  lplncvrlvol  40371  lncvrelatN  40536  pmapjoin  40607  pmapjat1  40608  pclclN  40646  osumclN  40722  lhprelat3N  40795  cdlemd5  40957  cdleme32fvcl  41195  cdlemg39  41471  ltrncom  41493  dihmeetALTN  42082  dochss  42120  mapdrvallem2  42400  nacsfix  43426  mzpsubst  43462  diophrw  43473  lzunuz  43482  jm2.19  43703  jm2.27  43718  hbtlem5  43838  tfsconcatrn  44052  nadd2rabtr  44094  fzunt  44164  iunrelexpuztr  44428  grumnudlem  44978  rfcnnnub  45739  3adantll2  45744  infleinf  46070  iccintsng  46222  mullimc  46315  mullimcf  46322  limcperiod  46327  cncfshift  46571  cncfperiod  46576  icccncfext  46584  stoweidlem20  46717  stoweidlem61  46758  fourierdlem73  46876  rmsupp0  49131  rmsuppss  49133  itschlc0xyqsol1  49529  itschlc0xyqsol  49530