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  17865  isprmidlc  21633  ssdifidlprm  21647  2sqmo  27769  tgbtwnconn1  29043  legso  29067  miriso  29147  footexALT  29198  footex  29201  opphl  29235  lnopp2hpgb  29246  tgaaddcpbllem1  29354  tgaaddcpbl  29357  cgrabasimass  29383  angmgmaddcpbl  29395  angmgmaddcl  29396  angmgmaddlid  29397  angmgmaddrid  29398  prlngmolem2  29436  f1otrg  29453  2ndresdju  33290  cyc3genpm  33759  cyc3conja  33764  rloccring  33878  mxidlprm  34041  qsdrngi  34065  1arithidom  34115  fldext2chn  34406  constrconj  34423  constrfin  34424  constrelextdg2  34425  zarcmplem  34559  afsval  35349  dffltz  43763  smfmullem3  47896  chnerlem1  47985