Theorem ad6antr 749

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ad7antr  751  ad7antlr  752  simp-6l  799  catass  17866  funcpropd  18083  natpropd  18160  ghmqusnsg  19502  ghmquskerlem3  19506  rhmqusnsg  21587  ssdifidllem  21646  ssdifidlprm  21648  matunitlindflem1  23000  restutop  24562  utopreg  24577  restmetu  24895  lgamucov  27371  istrkgcb  28924  tgsegconeu  28955  tgifscgr  28977  tgbtwnconn1lem3  29043  legtrd  29058  miriso  29148  footexALT  29199  footex  29202  opphllem3  29231  opphl  29236  plng3p  29281  trgcopy  29317  cgratr  29336  zerocgra  29337  dfcgra2  29344  ragcgra  29349  ragsupplcgra  29351  tgaaddcpbllem1  29355  inaghl  29370  cgrg3col4  29378  cgraer  29383  angmgmaddeu1  29385  angmgmaddcpbl  29396  angmgmaddcl  29397  angmgmaddlid  29398  prlngmolem2  29437  f1otrge  29455  clwlkclwwlklem2  30597  gsumwun  33684  cyc3genpm  33760  elrgspnlem4  33853  erler  33873  rlocaddval  33877  rlocmulval  33878  rloccring  33879  rhmquskerlem  34022  elrspunidl  34025  rhmimaidl  34029  mxidlirredi  34043  mxidlirred  34044  ssmxidllem  34045  qsdrngi  34066  dflringlem2  34074  1arithidom  34116  1arithufdlem3  34125  r1plmhm  34188  r1pquslmic  34189  lbsdiflsp0  34305  dimkerim  34306  fedgmul  34310  fldextrspunlsplem  34352  fldext2chn  34407  constrextdg2lem  34427  txomap  34513  heicant  38667  mblfinlem3  38671  primrootscoprmpow  43243  aks6d1c2lem4  43271  aks6d1c5  43283  limclner  46755  hoidmvle  47704  chnerlem1  47986