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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  f1prex  7304  poxp3  8175  naddsuc2  8739  ordiso2  9555  iunfictbso  10154  fin1a2lem12  10451  fin1a2lem13  10452  prlem934  11073  ifle  13239  xlesubadd  13305  icoshftf1o  13514  elfzonelfzo  13808  fsuppmapnn0fiub0  14034  swrdcl  14683  repswccat  14824  subcn2  15631  rpdvds  16697  coprmprod  16698  qexpz  16939  ramval  17046  0ram  17058  cshwrepswhash1  17140  mreexexd  17691  gsmsymgreqlem1  19448  pmtrf  19473  odmulg  19574  pgpfi1  19613  lsmcl  21082  lbsextlem3  21162  islindf4  21858  coe1mul2  22272  cramerlem2  22694  cpmadugsumlemF  22882  cayhamlem4  22894  iscnp4  23271  cnpnei  23272  cnconst2  23291  cnpdis  23301  cnhaus  23362  ordthauslem  23391  clsconn  23438  nlly2i  23484  txcn  23634  ordthmeolem  23809  flimrest  23991  isfcf  24042  alexsubALTlem4  24058  ghmcnp  24123  utop2nei  24259  blssps  24434  blss  24435  metcnp3  24553  metcnp  24554  xrsxmet  24831  metdseq0  24876  xrhmeo  24977  cfil3i  25303  caucfil  25317  cfilres  25330  fta1b  26211  mumul  27224  lgsfcl2  27347  lgsdir  27376  lgsne0  27379  nolt02o  27740  nogt01o  27741  nosupbnd1lem3  27755  nosupbnd1lem4  27756  nosupbnd1lem5  27757  nosupbnd2  27761  noinfbnd1lem3  27770  noinfbnd1lem4  27771  noinfbnd1lem5  27772  noinfbnd2  27776  sleadd1  28022  sltmul2  28197  istrkgcb  28464  axbtwnid  28954  axcontlem2  28980  axcontlem4  28982  axcontlem7  28985  axcontlem8  28986  umgr2v2enb1  29544  frgr3v  30294  extwwlkfab  30371  pjhthmo  31321  xrge0adddir  33023  archiabl  33205  dimvalfi  33652  pcmplfinf  33860  probun  34421  cnpconn  35235  satfv1lem  35367  outsideofeq  36131  linethru  36154  weiunso  36467  atlatmstc  39320  cvlcvr1  39340  ishlat3N  39355  hlrelat  39404  intnatN  39409  cvrval5  39417  atcvrlln  39522  llnexatN  39523  2at0mat0  39527  llncvrlpln  39560  lplnexllnN  39566  lplncvrlvol  39618  lncvrelatN  39783  pmapjoin  39854  pmapjat1  39855  pclclN  39893  osumclN  39969  lhprelat3N  40042  cdlemd5  40204  cdleme32fvcl  40442  cdlemg39  40718  ltrncom  40740  dihmeetALTN  41329  dochss  41367  mapdrvallem2  41647  nacsfix  42723  mzpsubst  42759  diophrw  42770  lzunuz  42779  jm2.19  43005  jm2.27  43020  hbtlem5  43140  tfsconcatrn  43355  nadd2rabtr  43397  fzunt  43468  iunrelexpuztr  43732  grumnudlem  44304  rfcnnnub  45041  3adantll2  45046  infleinf  45383  iccintsng  45536  mullimc  45631  mullimcf  45638  limcperiod  45643  cncfshift  45889  cncfperiod  45894  icccncfext  45902  stoweidlem20  46035  stoweidlem61  46076  fourierdlem73  46194  rmsupp0  48284  rmsuppss  48286  itschlc0xyqsol1  48687  itschlc0xyqsol  48688