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  7259  poxp3  8129  naddsuc2  8665  ordiso2  9468  iunfictbso  10067  fin1a2lem12  10364  fin1a2lem13  10365  prlem934  10986  ifle  13157  xlesubadd  13223  icoshftf1o  13435  elfzonelfzo  13730  fsuppmapnn0fiub0  13958  swrdcl  14610  repswccat  14751  subcn2  15561  rpdvds  16630  coprmprod  16631  qexpz  16872  ramval  16979  0ram  16991  cshwrepswhash1  17073  mreexexd  17609  gsmsymgreqlem1  19360  pmtrf  19385  odmulg  19486  pgpfi1  19525  lsmcl  20990  lbsextlem3  21070  islindf4  21747  coe1mul2  22155  cramerlem2  22575  cpmadugsumlemF  22763  cayhamlem4  22775  iscnp4  23150  cnpnei  23151  cnconst2  23170  cnpdis  23180  cnhaus  23241  ordthauslem  23270  clsconn  23317  nlly2i  23363  txcn  23513  ordthmeolem  23688  flimrest  23870  isfcf  23921  alexsubALTlem4  23937  ghmcnp  24002  utop2nei  24138  blssps  24312  blss  24313  metcnp3  24428  metcnp  24429  xrsxmet  24698  metdseq0  24743  xrhmeo  24844  cfil3i  25169  caucfil  25183  cfilres  25196  fta1b  26077  mumul  27091  lgsfcl2  27214  lgsdir  27243  lgsne0  27246  nolt02o  27607  nogt01o  27608  nosupbnd1lem3  27622  nosupbnd1lem4  27623  nosupbnd1lem5  27624  nosupbnd2  27628  noinfbnd1lem3  27637  noinfbnd1lem4  27638  noinfbnd1lem5  27639  noinfbnd2  27643  sleadd1  27896  sltmul2  28074  istrkgcb  28383  axbtwnid  28866  axcontlem2  28892  axcontlem4  28894  axcontlem7  28897  axcontlem8  28898  umgr2v2enb1  29454  frgr3v  30204  extwwlkfab  30281  pjhthmo  31231  xrge0adddir  32959  archiabl  33152  dimvalfi  33597  pcmplfinf  33851  probun  34410  cnpconn  35217  satfv1lem  35349  outsideofeq  36118  linethru  36141  weiunso  36454  atlatmstc  39312  cvlcvr1  39332  ishlat3N  39347  hlrelat  39396  intnatN  39401  cvrval5  39409  atcvrlln  39514  llnexatN  39515  2at0mat0  39519  llncvrlpln  39552  lplnexllnN  39558  lplncvrlvol  39610  lncvrelatN  39775  pmapjoin  39846  pmapjat1  39847  pclclN  39885  osumclN  39961  lhprelat3N  40034  cdlemd5  40196  cdleme32fvcl  40434  cdlemg39  40710  ltrncom  40732  dihmeetALTN  41321  dochss  41359  mapdrvallem2  41639  nacsfix  42700  mzpsubst  42736  diophrw  42747  lzunuz  42756  jm2.19  42982  jm2.27  42997  hbtlem5  43117  tfsconcatrn  43331  nadd2rabtr  43373  fzunt  43444  iunrelexpuztr  43708  grumnudlem  44274  rfcnnnub  45030  3adantll2  45035  infleinf  45368  iccintsng  45521  mullimc  45614  mullimcf  45621  limcperiod  45626  cncfshift  45872  cncfperiod  45877  icccncfext  45885  stoweidlem20  46018  stoweidlem61  46059  fourierdlem73  46177  rmsupp0  48356  rmsuppss  48358  itschlc0xyqsol1  48755  itschlc0xyqsol  48756