Theorem ad7antr 738

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 736	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  740  ad8antlr  741  simp-7l  788  catpropd  17612  natpropd  17883  chnub  18525  ucncn  24197  tgcgrxfr  28494  tgbtwnconn1lem3  28550  tgbtwnconn1  28551  midexlem  28668  lnopp2hpgb  28739  trgcopy  28780  mgcf1o  32979  elrgspnlem4  33207  elrspunidl  33388  rhmimaidl  33392  qsidomlem2  33413  ssdifidlprm  33418  mxidlirredi  33431  1arithufdlem3  33506  lbsdiflsp0  33634  fedgmul  33639  constrconj  33753  constrelextdg2  33755  zarcmplem  33889  sigapildsys  34170  afsval  34679  matunitlindflem1  37655  aks6d1c2lem4  42159  dffltz  42666