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  17675  natpropd  17946  chnub  18588  ucncn  24249  tgcgrxfr  28586  tgbtwnconn1lem3  28642  tgbtwnconn1  28643  midexlem  28760  lnopp2hpgb  28831  trgcopy  28872  mgcf1o  33063  elrgspnlem4  33306  elrspunidl  33488  rhmimaidl  33492  qsidomlem2  33513  ssdifidlprm  33518  mxidlirredi  33531  1arithufdlem3  33606  lbsdiflsp0  33770  fedgmul  33775  constrconj  33889  constrelextdg2  33891  zarcmplem  34025  sigapildsys  34306  afsval  34815  matunitlindflem1  37937  aks6d1c2lem4  42566  dffltz  43067