Theorem ad7antr 751

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ad8antr  753  ad8antlr  754  simp-7l  801  catpropd  17790  natpropd  18061  chnub  18703  qsidomlem2  21518  ssdifidlprm  21523  ucncn  24478  tgcgrxfr  28824  tgbtwnconn1lem3  28880  tgbtwnconn1  28881  midexlem  29006  lnopp2hpgb  29082  trgcopy  29152  perpprlng  29237  prlngmolem1  29239  mgcf1o  33354  elrgspnlem4  33596  rlocisunit  33627  elrspunidl  33767  rhmimaidl  33771  mxidlirredi  33785  1arithufdlem3  33867  lbsdiflsp0  34047  fedgmul  34052  constrconj  34166  constrelextdg2  34168  zarcmplem  34302  sigapildsys  34584  afsval  35093  matunitlindflem1  38308  aks6d1c2lem4  42935  dffltz  43407