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  17632  natpropd  17903  chnub  18545  ucncn  24228  tgcgrxfr  28590  tgbtwnconn1lem3  28646  tgbtwnconn1  28647  midexlem  28764  lnopp2hpgb  28835  trgcopy  28876  mgcf1o  33085  elrgspnlem4  33327  elrspunidl  33509  rhmimaidl  33513  qsidomlem2  33534  ssdifidlprm  33539  mxidlirredi  33552  1arithufdlem3  33627  lbsdiflsp0  33783  fedgmul  33788  constrconj  33902  constrelextdg2  33904  zarcmplem  34038  sigapildsys  34319  afsval  34828  matunitlindflem1  37813  aks6d1c2lem4  42377  dffltz  42873