Theorem simpll3 1214

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1089

This theorem is referenced by:  f1prex  7284  poxp3  8138  ordiso2  9512  iunfictbso  10111  fin1a2lem12  10408  fin1a2lem13  10409  prlem934  11030  ifle  13180  xlesubadd  13246  icoshftf1o  13455  elfzonelfzo  13738  fsuppmapnn0fiub0  13962  swrdcl  14599  repswccat  14740  subcn2  15543  rpdvds  16601  coprmprod  16602  qexpz  16838  ramval  16945  0ram  16957  cshwrepswhash1  17040  mreexexd  17596  gsmsymgreqlem1  19339  pmtrf  19364  odmulg  19465  pgpfi1  19504  lsmcl  20838  lbsextlem3  20918  islindf4  21612  coe1mul2  22011  cramerlem2  22410  cpmadugsumlemF  22598  cayhamlem4  22610  iscnp4  22987  cnpnei  22988  cnconst2  23007  cnpdis  23017  cnhaus  23078  ordthauslem  23107  clsconn  23154  nlly2i  23200  txcn  23350  ordthmeolem  23525  flimrest  23707  isfcf  23758  alexsubALTlem4  23774  ghmcnp  23839  utop2nei  23975  blssps  24150  blss  24151  metcnp3  24269  metcnp  24270  xrsxmet  24545  metdseq0  24590  xrhmeo  24686  cfil3i  25010  caucfil  25024  cfilres  25037  fta1b  25911  mumul  26909  lgsfcl2  27030  lgsdir  27059  lgsne0  27062  nolt02o  27422  nogt01o  27423  nosupbnd1lem3  27437  nosupbnd1lem4  27438  nosupbnd1lem5  27439  nosupbnd2  27443  noinfbnd1lem3  27452  noinfbnd1lem4  27453  noinfbnd1lem5  27454  noinfbnd2  27458  sleadd1  27699  sltmul2  27850  istrkgcb  27962  axbtwnid  28452  axcontlem2  28478  axcontlem4  28480  axcontlem7  28483  axcontlem8  28484  umgr2v2enb1  29038  frgr3v  29783  extwwlkfab  29860  pjhthmo  30810  xrge0adddir  32448  archiabl  32602  dimvalfi  32962  pcmplfinf  33127  probun  33704  cnpconn  34507  satfv1lem  34639  outsideofeq  35394  linethru  35417  atlatmstc  38492  cvlcvr1  38512  ishlat3N  38527  hlrelat  38576  intnatN  38581  cvrval5  38589  atcvrlln  38694  llnexatN  38695  2at0mat0  38699  llncvrlpln  38732  lplnexllnN  38738  lplncvrlvol  38790  lncvrelatN  38955  pmapjoin  39026  pmapjat1  39027  pclclN  39065  osumclN  39141  lhprelat3N  39214  cdlemd5  39376  cdleme32fvcl  39614  cdlemg39  39890  ltrncom  39912  dihmeetALTN  40501  dochss  40539  mapdrvallem2  40819  nacsfix  41752  mzpsubst  41788  diophrw  41799  lzunuz  41808  jm2.19  42034  jm2.27  42049  hbtlem5  42172  tfsconcatrn  42394  nadd2rabtr  42436  naddsuc2  42445  fzunt  42508  iunrelexpuztr  42772  grumnudlem  43346  rfcnnnub  44022  3adantll2  44027  infleinf  44381  iccintsng  44535  mullimc  44631  mullimcf  44638  limcperiod  44643  cncfshift  44889  cncfperiod  44894  icccncfext  44902  stoweidlem20  45035  stoweidlem61  45076  fourierdlem73  45194  rmsupp0  47133  rmsuppss  47135  itschlc0xyqsol1  47540  itschlc0xyqsol  47541