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  17780  isprmidlc  21541  ssdifidlprm  21555  2sqmo  27681  tgbtwnconn1  28925  legso  28949  miriso  29029  footexALT  29080  footex  29083  opphl  29117  lnopp2hpgb  29128  tgaaddcpbllem1  29236  tgaaddcpbl  29239  cgrabasimass  29265  angmgmaddcpbl  29277  angmgmaddcl  29278  angmgmaddlid  29279  angmgmaddrid  29280  prlngmolem2  29318  f1otrg  29335  2ndresdju  33130  cyc3genpm  33600  cyc3conja  33605  rloccring  33719  mxidlprm  33881  qsdrngi  33905  1arithidom  33955  fldext2chn  34246  constrconj  34263  constrfin  34264  constrelextdg2  34265  zarcmplem  34399  afsval  35190  dffltz  43488  smfmullem3  47629  chnerlem1  47718