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  17666  natpropd  17937  chnub  18579  ucncn  24259  tgcgrxfr  28600  tgbtwnconn1lem3  28656  tgbtwnconn1  28657  midexlem  28774  lnopp2hpgb  28845  trgcopy  28886  mgcf1o  33078  elrgspnlem4  33321  elrspunidl  33503  rhmimaidl  33507  qsidomlem2  33528  ssdifidlprm  33533  mxidlirredi  33546  1arithufdlem3  33621  lbsdiflsp0  33786  fedgmul  33791  constrconj  33905  constrelextdg2  33907  zarcmplem  34041  sigapildsys  34322  afsval  34831  matunitlindflem1  37951  aks6d1c2lem4  42580  dffltz  43081