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 739	1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  f1prex  7290  poxp3  8160  naddsuc2  8704  ordiso2  9502  iunfictbso  10186  fin1a2lem12  10482  fin1a2lem13  10483  prlem934  11111  ifle  13320  xlesubadd  13386  icoshftf1o  13598  elfzonelfzo  13897  fsuppmapnn0fiub0  14129  swrdcl  14786  repswccat  14930  subcn2  15755  rpdvds  16828  coprmprod  16829  qexpz  17072  ramval  17179  0ram  17191  cshwrepswhash1  17273  mreexexd  17815  gsmsymgreqlem1  19637  pmtrf  19662  odmulg  19763  pgpfi1  19802  lsmcl  21351  lbsextlem3  21431  islindf4  22137  coe1mul2  22581  cramerlem2  22999  cpmadugsumlemF  23187  cayhamlem4  23199  iscnp4  23574  cnpnei  23575  cnconst2  23594  cnpdis  23604  cnhaus  23665  ordthauslem  23694  clsconn  23741  nlly2i  23788  txcn  23938  ordthmeolem  24113  flimrest  24295  isfcf  24346  alexsubALTlem4  24362  ghmcnp  24427  utop2nei  24562  blssps  24736  blss  24737  metcnp3  24852  metcnp  24853  xrsxmet  25122  metdseq0  25167  xrhmeo  25260  cfil3i  25583  caucfil  25597  cfilres  25610  fta1b  26483  mumul  27501  lgsfcl2  27623  lgsdir  27652  lgsne0  27655  nolt02o  28045  nogt01o  28046  nosupbnd1lem3  28060  nosupbnd1lem4  28061  nosupbnd1lem5  28062  nosupbnd2  28066  noinfbnd1lem3  28075  noinfbnd1lem4  28076  noinfbnd1lem5  28077  noinfbnd2  28081  leadds1  28368  ltmuls2  28550  istrkgcb  28911  axbtwnid  29510  axcontlem2  29536  axcontlem4  29538  axcontlem7  29541  axcontlem8  29542  umgr2v2enb1  30100  frgr3v  30869  extwwlkfab  30946  pjhthmo  31897  xrge0adddir  33572  archiabl  33752  dimvalfi  34227  pcmplfinf  34486  probun  35044  cnpconn  35974  satfv1lem  36106  outsideofeq  36875  linethru  36898  weiunso  37234  atlatmstc  40356  cvlcvr1  40376  ishlat3N  40391  hlrelat  40439  intnatN  40444  cvrval5  40452  atcvrlln  40557  llnexatN  40558  2at0mat0  40562  llncvrlpln  40595  lplnexllnN  40601  lplncvrlvol  40653  lncvrelatN  40818  pmapjoin  40889  pmapjat1  40890  pclclN  40928  osumclN  41004  lhprelat3N  41077  cdlemd5  41239  cdleme32fvcl  41477  cdlemg39  41753  ltrncom  41775  dihmeetALTN  42364  dochss  42402  mapdrvallem2  42682  nacsfix  43702  mzpsubst  43738  diophrw  43749  lzunuz  43758  jm2.19  43979  jm2.27  43994  hbtlem5  44114  tfsconcatrn  44328  nadd2rabtr  44370  fzunt  44440  iunrelexpuztr  44704  grumnudlem  45254  rfcnnnub  46022  3adantll2  46027  infleinf  46352  iccintsng  46504  mullimc  46597  mullimcf  46604  limcperiod  46609  cncfshift  46853  cncfperiod  46858  icccncfext  46866  stoweidlem20  46999  stoweidlem61  47040  fourierdlem73  47158  rmsupp0  49449  rmsuppss  49451  itschlc0xyqsol1  49847  itschlc0xyqsol  49848