Theorem simp-7r 788

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

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  catass  17669  2sqmo  27415  tgbtwnconn1  28451  legso  28475  miriso  28546  footexALT  28594  footex  28597  opphl  28630  lnopp2hpgb  28639  f1otrg  28747  2ndresdju  32516  cyc3genpm  32965  cyc3conja  32970  rloccring  33060  isprmidlc  33259  ssdifidlprm  33270  mxidlprm  33282  qsdrngi  33307  1arithidom  33349  zarcmplem  33613  afsval  34434  dffltz  42193  smfmullem3  46319