Theorem ad7antr 739

Description: Deduction adding 7 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.)

Hypothesis

Ref	Expression
ad2ant.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
ad7antr	⊢ ((((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) → 𝜓)

Proof of Theorem ad7antr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
3	2	ad6antr 737	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:  ad8antr  741  ad8antlr  742  simp-7l  789  catpropd  17644  natpropd  17915  chnub  18557  ucncn  24240  tgcgrxfr  28602  tgbtwnconn1lem3  28658  tgbtwnconn1  28659  midexlem  28776  lnopp2hpgb  28847  trgcopy  28888  mgcf1o  33095  elrgspnlem4  33338  elrspunidl  33520  rhmimaidl  33524  qsidomlem2  33545  ssdifidlprm  33550  mxidlirredi  33563  1arithufdlem3  33638  lbsdiflsp0  33803  fedgmul  33808  constrconj  33922  constrelextdg2  33924  zarcmplem  34058  sigapildsys  34339  afsval  34848  matunitlindflem1  37861  aks6d1c2lem4  42491  dffltz  42986