Theorem ad6antr 732

Description: Deduction adding 6 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
ad6antr	⊢ (((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) → 𝜓)

Proof of Theorem ad6antr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	adantr 479	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
3	2	ad5antr 730	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:  ad7antr  734  ad7antlr  735  simp-6l  783  catass  17634  funcpropd  17855  natpropd  17933  restutop  23962  utopreg  23977  restmetu  24299  lgamucov  26778  istrkgcb  27974  tgifscgr  28026  tgbtwnconn1lem3  28092  legtrd  28107  miriso  28188  footexALT  28236  footex  28239  opphllem3  28267  opphl  28272  trgcopy  28322  cgratr  28341  dfcgra2  28348  inaghl  28363  cgrg3col4  28371  f1otrge  28390  clwlkclwwlklem2  29520  cyc3genpm  32581  ghmquskerlem3  32805  rhmquskerlem  32817  elrspunidl  32820  rhmimaidl  32824  mxidlirredi  32861  mxidlirred  32862  ssmxidllem  32863  qsdrngi  32883  r1plmhm  32955  r1pquslmic  32956  lbsdiflsp0  32999  dimkerim  33000  fedgmul  33004  txomap  33112  matunitlindflem1  36787  heicant  36826  mblfinlem3  36830  limclner  44665  hoidmvle  45614