Theorem simp-7r 802

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

Assertion

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

Proof of Theorem simp-7r

Step	Hyp	Ref	Expression
1		id 23	. 2 ⊢ (𝜓 → 𝜓)
2	1	ad7antlr 752	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  17889  isprmidlc  21658  ssdifidlprm  21672  2sqmo  27794  tgbtwnconn1  29068  legso  29092  miriso  29172  footexALT  29223  footex  29226  opphl  29260  lnopp2hpgb  29271  tgaaddcpbllem1  29379  tgaaddcpbl  29382  cgrabasimass  29408  angmgmaddcpbl  29420  angmgmaddcl  29421  angmgmaddlid  29422  angmgmaddrid  29423  prlngmolem2  29461  f1otrg  29478  2ndresdju  33315  cyc3genpm  33783  cyc3conja  33788  rloccring  33902  mxidlprm  34065  qsdrngi  34089  1arithidom  34139  fldext2chn  34430  constrconj  34447  constrfin  34448  constrelextdg2  34449  zarcmplem  34583  afsval  35373  dffltz  43863  smfmullem3  48008  chnerlem1  48097