Theorem ad6antr 733

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 481	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
3	2	ad5antr 731	1 ⊢ (((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  ad7antr  735  ad7antlr  736  simp-6l  784  catass  17492  funcpropd  17713  natpropd  17791  restutop  23495  utopreg  23510  restmetu  23832  lgamucov  26293  istrkgcb  27106  tgifscgr  27158  tgbtwnconn1lem3  27224  legtrd  27239  miriso  27320  footexALT  27368  footex  27371  opphllem3  27399  opphl  27404  trgcopy  27454  cgratr  27473  dfcgra2  27480  inaghl  27495  cgrg3col4  27503  f1otrge  27522  clwlkclwwlklem2  28652  cyc3genpm  31706  elrspunidl  31903  rhmimaidl  31906  ssmxidllem  31938  lbsdiflsp0  32005  dimkerim  32006  fedgmul  32010  txomap  32082  matunitlindflem1  35878  heicant  35917  mblfinlem3  35921  limclner  43528  hoidmvle  44475