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  17621  2sqmo  27416  tgbtwnconn1  28659  legso  28683  miriso  28754  footexALT  28802  footex  28805  opphl  28838  lnopp2hpgb  28847  f1otrg  28955  2ndresdju  32738  cyc3genpm  33245  cyc3conja  33250  rloccring  33363  isprmidlc  33539  ssdifidlprm  33550  mxidlprm  33562  qsdrngi  33587  1arithidom  33629  fldext2chn  33905  constrconj  33922  constrfin  33923  constrelextdg2  33924  zarcmplem  34058  afsval  34848  dffltz  42989  smfmullem3  47148  chnerlem1  47237