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  17677  natpropd  17948  chnub  18590  ucncn  24251  tgcgrxfr  28588  tgbtwnconn1lem3  28644  tgbtwnconn1  28645  midexlem  28762  lnopp2hpgb  28833  trgcopy  28874  mgcf1o  33065  elrgspnlem4  33308  elrspunidl  33490  rhmimaidl  33494  qsidomlem2  33515  ssdifidlprm  33520  mxidlirredi  33533  1arithufdlem3  33608  lbsdiflsp0  33772  fedgmul  33777  constrconj  33891  constrelextdg2  33893  zarcmplem  34027  sigapildsys  34308  afsval  34817  matunitlindflem1  37939  aks6d1c2lem4  42568  dffltz  43069