Theorem simp-7r 801

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 751	1 ⊢ ((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  catass  17743  isprmidlc  21453  ssdifidlprm  21467  2sqmo  27579  tgbtwnconn1  28822  legso  28846  miriso  28925  footexALT  28976  footex  28979  opphl  29013  lnopp2hpgb  29023  prlngmolem2  29181  f1otrg  29198  2ndresdju  32972  cyc3genpm  33450  cyc3conja  33455  rloccring  33569  mxidlprm  33731  qsdrngi  33755  1arithidom  33805  fldext2chn  34096  constrconj  34113  constrfin  34114  constrelextdg2  34115  zarcmplem  34249  afsval  35039  dffltz  43346  smfmullem3  47487  chnerlem1  47578