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  7224  poxp3  8086  naddsuc2  8622  ordiso2  9408  iunfictbso  10012  fin1a2lem12  10309  fin1a2lem13  10310  prlem934  10931  ifle  13098  xlesubadd  13164  icoshftf1o  13376  elfzonelfzo  13671  fsuppmapnn0fiub0  13902  swrdcl  14555  repswccat  14695  subcn2  15504  rpdvds  16573  coprmprod  16574  qexpz  16815  ramval  16922  0ram  16934  cshwrepswhash1  17016  mreexexd  17556  gsmsymgreqlem1  19344  pmtrf  19369  odmulg  19470  pgpfi1  19509  lsmcl  21019  lbsextlem3  21099  islindf4  21777  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  28919  axcontlem2  28945  axcontlem4  28947  axcontlem7  28950  axcontlem8  28951  umgr2v2enb1  29507  frgr3v  30257  extwwlkfab  30334  pjhthmo  31284  xrge0adddir  33006  archiabl  33174  dimvalfi  33635  pcmplfinf  33895  probun  34453  cnpconn  35295  satfv1lem  35427  outsideofeq  36195  linethru  36218  weiunso  36531  atlatmstc  39439  cvlcvr1  39459  ishlat3N  39474  hlrelat  39522  intnatN  39527  cvrval5  39535  atcvrlln  39640  llnexatN  39641  2at0mat0  39645  llncvrlpln  39678  lplnexllnN  39684  lplncvrlvol  39736  lncvrelatN  39901  pmapjoin  39972  pmapjat1  39973  pclclN  40011  osumclN  40087  lhprelat3N  40160  cdlemd5  40322  cdleme32fvcl  40560  cdlemg39  40836  ltrncom  40858  dihmeetALTN  41447  dochss  41485  mapdrvallem2  41765  nacsfix  42830  mzpsubst  42866  diophrw  42877  lzunuz  42886  jm2.19  43111  jm2.27  43126  hbtlem5  43246  tfsconcatrn  43460  nadd2rabtr  43502  fzunt  43573  iunrelexpuztr  43837  grumnudlem  44403  rfcnnnub  45158  3adantll2  45163  infleinf  45495  iccintsng  45648  mullimc  45741  mullimcf  45748  limcperiod  45753  cncfshift  45997  cncfperiod  46002  icccncfext  46010  stoweidlem20  46143  stoweidlem61  46184  fourierdlem73  46302  rmsupp0  48493  rmsuppss  48495  itschlc0xyqsol1  48892  itschlc0xyqsol  48893