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  17863  natpropd  18134  chnub  18776  qsidomlem2  21617  ssdifidlprm  21622  matunitlindflem1  22974  ucncn  24583  tgcgrxfr  28963  tgbtwnconn1lem3  29019  tgbtwnconn1  29020  midexlem  29146  lnopp2hpgb  29223  trgcopy  29293  tgaaddcpbl  29334  cgraer  29359  cgrabasimass  29360  angmgmaddeu1  29361  angmgmaddcpbl  29372  angmgmaddcl  29373  angmgmaddrid  29375  perpprlng  29410  prlngmolem1  29412  mgcf1o  33546  elrgspnlem4  33788  rlocisunit  33819  elrspunidl  33960  rhmimaidl  33964  mxidlirredi  33978  1arithufdlem3  34060  lbsdiflsp0  34240  fedgmul  34245  constrconj  34359  constrelextdg2  34361  zarcmplem  34495  sigapildsys  34777  afsval  35286  aks6d1c2lem4  43145  dffltz  43624