Theorem ad7antr 736

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

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  ad8antr  738  ad8antlr  739  simp-7l  787  catpropd  17743  natpropd  18022  ucncn  24304  tgcgrxfr  28468  tgbtwnconn1lem3  28524  tgbtwnconn1  28525  midexlem  28642  lnopp2hpgb  28713  trgcopy  28754  mgcf1o  32901  chnub  32909  elrspunidl  33334  rhmimaidl  33338  qsidomlem2  33359  ssdifidlprm  33364  mxidlirredi  33377  1arithufdlem3  33452  lbsdiflsp0  33552  fedgmul  33557  constrconj  33642  constrelextdg2  33644  zarcmplem  33734  sigapildsys  34033  afsval  34555  matunitlindflem1  37364  aks6d1c2lem4  41873  dffltz  42358