Theorem simp-7r 790

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 22	. 2 ⊢ (𝜓 → 𝜓)
2	1	ad7antlr 740	1 ⊢ ((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395

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

This theorem is referenced by:  catass  17652  2sqmo  27400  tgbtwnconn1  28643  legso  28667  miriso  28738  footexALT  28786  footex  28789  opphl  28822  lnopp2hpgb  28831  f1otrg  28939  2ndresdju  32722  cyc3genpm  33213  cyc3conja  33218  rloccring  33331  isprmidlc  33507  ssdifidlprm  33518  mxidlprm  33530  qsdrngi  33555  1arithidom  33597  fldext2chn  33872  constrconj  33889  constrfin  33890  constrelextdg2  33891  zarcmplem  34025  afsval  34815  dffltz  43067  smfmullem3  47221  chnerlem1  47312