Theorem simp-7r 789

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  catass  17654  2sqmo  27355  tgbtwnconn1  28509  legso  28533  miriso  28604  footexALT  28652  footex  28655  opphl  28688  lnopp2hpgb  28697  f1otrg  28805  2ndresdju  32580  cyc3genpm  33116  cyc3conja  33121  rloccring  33228  isprmidlc  33425  ssdifidlprm  33436  mxidlprm  33448  qsdrngi  33473  1arithidom  33515  fldext2chn  33725  constrconj  33742  constrfin  33743  constrelextdg2  33744  zarcmplem  33878  afsval  34669  dffltz  42629  smfmullem3  46798