Theorem simp-6r 800

Description: Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.)

Assertion

Ref	Expression
simp-6r	⊢ (((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)

Proof of Theorem simp-6r

Step	Hyp	Ref	Expression
1		id 23	. 2 ⊢ (𝜓 → 𝜓)
2	1	ad6antlr 750	1 ⊢ (((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  catass  17892  chnub  18828  mhmmnd  19306  rhmqusnsg  21614  ssdifidllem  21673  ssdifidlprm  21675  scmatscm  22861  cfilucfil  24911  2sqmo  27797  tgsegconeu  28982  tgbtwnconn1  29071  legso  29095  footexALT  29226  opphl  29263  trgcopy  29344  zerocgra  29364  dfcgra2  29371  ragcgra  29376  tgaaddcpbllem1  29382  cgrg3col4  29405  cgraer  29410  cgrabasimass  29411  angmgmaddcpbl  29423  angmgmaddcl  29424  angmgmaddlid  29425  angmgmaddrid  29426  prlngex  29462  prlngmolem2  29464  f1otrg  29481  2ndresdju  33318  cyc3genpm  33789  cyc3conja  33794  rloccring  33908  edompidlem  33940  rhmquskerlem  34059  rhmimaidl  34066  mxidlirredi  34080  ssmxidllem  34082  1arithidom  34153  1arithufdlem3  34162  r1plmhm  34224  r1pquslmic  34225  fldextrspunlsplem  34388  fldext2chn  34443  constrconj  34460  constrfin  34461  constrelextdg2  34462  cos9thpiminplylem2  34498  pstmxmet  34612  signstfvneq0  35284  afsval  35386  mblfinlem3  38782  mblfinlem4  38783  primrootscoprmpow  43352  aks6d1c2lem4  43380  dffltz  43874  iunconnlem2  46119  suplesup  46566  limclner  46876  fourierdlem51  47382  hoidmvle  47825  smfmullem3  48018  chnerlem1  48107  upfval  50507