Theorem simp-7r 795

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  catass  17650  2sqmo  27425  tgbtwnconn1  28668  legso  28692  miriso  28763  footexALT  28811  footex  28814  opphl  28847  lnopp2hpgb  28856  f1otrg  28964  2ndresdju  32748  cyc3genpm  33240  cyc3conja  33245  rloccring  33358  isprmidlc  33537  ssdifidlprm  33548  mxidlprm  33560  qsdrngi  33585  1arithidom  33627  fldext2chn  33919  constrconj  33936  constrfin  33937  constrelextdg2  33938  zarcmplem  34072  afsval  34862  dffltz  43091  smfmullem3  47243  chnerlem1  47334