Theorem simpll3 1231

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

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

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 1103

This theorem is referenced by:  f1prex  7272  poxp3  8134  naddsuc2  8676  ordiso2  9465  iunfictbso  10086  fin1a2lem12  10383  fin1a2lem13  10384  prlem934  11006  ifle  13211  xlesubadd  13277  icoshftf1o  13489  elfzonelfzo  13786  fsuppmapnn0fiub0  14017  swrdcl  14671  repswccat  14811  subcn2  15634  rpdvds  16706  coprmprod  16707  qexpz  16949  ramval  17056  0ram  17068  cshwrepswhash1  17150  mreexexd  17692  gsmsymgreqlem1  19488  pmtrf  19513  odmulg  19614  pgpfi1  19653  lsmcl  21170  lbsextlem3  21250  islindf4  21945  coe1mul2  22387  cramerlem2  22802  cpmadugsumlemF  22990  cayhamlem4  23002  iscnp4  23377  cnpnei  23378  cnconst2  23397  cnpdis  23407  cnhaus  23468  ordthauslem  23497  clsconn  23544  nlly2i  23590  txcn  23740  ordthmeolem  23915  flimrest  24097  isfcf  24148  alexsubALTlem4  24164  ghmcnp  24229  utop2nei  24364  blssps  24538  blss  24539  metcnp3  24654  metcnp  24655  xrsxmet  24924  metdseq0  24969  xrhmeo  25062  cfil3i  25385  caucfil  25399  cfilres  25412  fta1b  26286  mumul  27299  lgsfcl2  27421  lgsdir  27450  lgsne0  27453  nolt02o  27813  nogt01o  27814  nosupbnd1lem3  27828  nosupbnd1lem4  27829  nosupbnd1lem5  27830  nosupbnd2  27834  noinfbnd1lem3  27843  noinfbnd1lem4  27844  noinfbnd1lem5  27845  noinfbnd2  27849  leadds1  28136  ltmuls2  28318  istrkgcb  28679  axbtwnid  29194  axcontlem2  29220  axcontlem4  29222  axcontlem7  29225  axcontlem8  29226  umgr2v2enb1  29781  frgr3v  30531  extwwlkfab  30608  pjhthmo  31559  xrge0adddir  33246  archiabl  33426  dimvalfi  33904  pcmplfinf  34163  probun  34721  cnpconn  35588  satfv1lem  35720  outsideofeq  36488  linethru  36511  weiunso  36834  atlatmstc  39950  cvlcvr1  39970  ishlat3N  39985  hlrelat  40033  intnatN  40038  cvrval5  40046  atcvrlln  40151  llnexatN  40152  2at0mat0  40156  llncvrlpln  40189  lplnexllnN  40195  lplncvrlvol  40247  lncvrelatN  40412  pmapjoin  40483  pmapjat1  40484  pclclN  40522  osumclN  40598  lhprelat3N  40671  cdlemd5  40833  cdleme32fvcl  41071  cdlemg39  41347  ltrncom  41369  dihmeetALTN  41958  dochss  41996  mapdrvallem2  42276  nacsfix  43300  mzpsubst  43336  diophrw  43347  lzunuz  43356  jm2.19  43577  jm2.27  43592  hbtlem5  43712  tfsconcatrn  43926  nadd2rabtr  43968  fzunt  44038  iunrelexpuztr  44302  grumnudlem  44854  rfcnnnub  45615  3adantll2  45620  infleinf  45946  iccintsng  46098  mullimc  46191  mullimcf  46198  limcperiod  46203  cncfshift  46447  cncfperiod  46452  icccncfext  46460  stoweidlem20  46593  stoweidlem61  46634  fourierdlem73  46752  rmsupp0  49000  rmsuppss  49002  itschlc0xyqsol1  49398  itschlc0xyqsol  49399