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  17395  funcpropd  17616  natpropd  17694  restutop  23389  utopreg  23404  restmetu  23726  lgamucov  26187  istrkgcb  26817  tgifscgr  26869  tgbtwnconn1lem3  26935  legtrd  26950  miriso  27031  footexALT  27079  footex  27082  opphllem3  27110  opphl  27115  trgcopy  27165  cgratr  27184  dfcgra2  27191  inaghl  27206  cgrg3col4  27214  f1otrge  27233  clwlkclwwlklem2  28364  cyc3genpm  31419  elrspunidl  31606  rhmimaidl  31609  ssmxidllem  31641  lbsdiflsp0  31707  dimkerim  31708  fedgmul  31712  txomap  31784  matunitlindflem1  35773  heicant  35812  mblfinlem3  35816  limclner  43192  hoidmvle  44138