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  17610  2sqmo  27364  tgbtwnconn1  28538  legso  28562  miriso  28633  footexALT  28681  footex  28684  opphl  28717  lnopp2hpgb  28726  f1otrg  28834  2ndresdju  32606  cyc3genpm  33107  cyc3conja  33112  rloccring  33223  isprmidlc  33397  ssdifidlprm  33408  mxidlprm  33420  qsdrngi  33445  1arithidom  33487  fldext2chn  33697  constrconj  33714  constrfin  33715  constrelextdg2  33716  zarcmplem  33850  afsval  34641  dffltz  42610  smfmullem3  46778