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  17840  isprmidlc  21608  ssdifidlprm  21622  2sqmo  27746  tgbtwnconn1  29020  legso  29044  miriso  29124  footexALT  29175  footex  29178  opphl  29212  lnopp2hpgb  29223  tgaaddcpbllem1  29331  tgaaddcpbl  29334  cgrabasimass  29360  angmgmaddcpbl  29372  angmgmaddcl  29373  angmgmaddlid  29374  angmgmaddrid  29375  prlngmolem2  29413  f1otrg  29430  2ndresdju  33225  cyc3genpm  33695  cyc3conja  33700  rloccring  33814  mxidlprm  33977  qsdrngi  34001  1arithidom  34051  fldext2chn  34342  constrconj  34359  constrfin  34360  constrelextdg2  34361  zarcmplem  34495  afsval  35286  dffltz  43624  smfmullem3  47747  chnerlem1  47836