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  17643  2sqmo  27414  tgbtwnconn1  28657  legso  28681  miriso  28752  footexALT  28800  footex  28803  opphl  28836  lnopp2hpgb  28845  f1otrg  28953  2ndresdju  32737  cyc3genpm  33228  cyc3conja  33233  rloccring  33346  isprmidlc  33522  ssdifidlprm  33533  mxidlprm  33545  qsdrngi  33570  1arithidom  33612  fldext2chn  33888  constrconj  33905  constrfin  33906  constrelextdg2  33907  zarcmplem  34041  afsval  34831  dffltz  43081  smfmullem3  47239  chnerlem1  47328