Theorem simp-7r 789

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 739	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  17647  2sqmo  27348  tgbtwnconn1  28502  legso  28526  miriso  28597  footexALT  28645  footex  28648  opphl  28681  lnopp2hpgb  28690  f1otrg  28798  2ndresdju  32573  cyc3genpm  33109  cyc3conja  33114  rloccring  33221  isprmidlc  33418  ssdifidlprm  33429  mxidlprm  33441  qsdrngi  33466  1arithidom  33508  fldext2chn  33718  constrconj  33735  constrfin  33736  constrelextdg2  33737  zarcmplem  33871  afsval  34662  dffltz  42622  smfmullem3  46791