Theorem ad7antr 750

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 485	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
3	2	ad6antr 748	1 ⊢ ((((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  ad8antr  752  ad8antlr  753  simp-7l  800  catpropd  17766  natpropd  18037  chnub  18679  qsidomlem2  21462  ssdifidlprm  21467  ucncn  24422  tgcgrxfr  28765  tgbtwnconn1lem3  28821  tgbtwnconn1  28822  midexlem  28947  lnopp2hpgb  29023  trgcopy  29093  perpprlng  29178  prlngmolem1  29180  mgcf1o  33301  elrgspnlem4  33543  rlocisunit  33574  elrspunidl  33714  rhmimaidl  33718  mxidlirredi  33732  1arithufdlem3  33814  lbsdiflsp0  33994  fedgmul  33999  constrconj  34113  constrelextdg2  34115  zarcmplem  34249  sigapildsys  34530  afsval  35039  matunitlindflem1  38245  aks6d1c2lem4  42872  dffltz  43346