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  17912  natpropd  18183  chnub  18825  qsidomlem2  21667  ssdifidlprm  21672  matunitlindflem1  23024  ucncn  24633  tgcgrxfr  29011  tgbtwnconn1lem3  29067  tgbtwnconn1  29068  midexlem  29194  lnopp2hpgb  29271  trgcopy  29341  tgaaddcpbl  29382  cgraer  29407  cgrabasimass  29408  angmgmaddeu1  29409  angmgmaddcpbl  29420  angmgmaddcl  29421  angmgmaddrid  29423  perpprlng  29458  prlngmolem1  29460  mgcf1o  33634  elrgspnlem4  33876  rlocisunit  33907  elrspunidl  34048  rhmimaidl  34052  mxidlirredi  34066  1arithufdlem3  34148  lbsdiflsp0  34328  fedgmul  34333  constrconj  34447  constrelextdg2  34449  zarcmplem  34583  sigapildsys  34865  afsval  35373  aks6d1c2lem4  43369  dffltz  43863