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  17840  funcpropd  18057  natpropd  18134  ghmqusnsg  19476  ghmquskerlem3  19480  rhmqusnsg  21561  ssdifidllem  21620  ssdifidlprm  21622  matunitlindflem1  22974  restutop  24536  utopreg  24551  restmetu  24869  lgamucov  27347  istrkgcb  28900  tgsegconeu  28931  tgifscgr  28953  tgbtwnconn1lem3  29019  legtrd  29034  miriso  29124  footexALT  29175  footex  29178  opphllem3  29207  opphl  29212  plng3p  29257  trgcopy  29293  cgratr  29312  zerocgra  29313  dfcgra2  29320  ragcgra  29325  ragsupplcgra  29327  tgaaddcpbllem1  29331  inaghl  29346  cgrg3col4  29354  cgraer  29359  angmgmaddeu1  29361  angmgmaddcpbl  29372  angmgmaddcl  29373  angmgmaddlid  29374  prlngmolem2  29413  f1otrge  29431  clwlkclwwlklem2  30573  gsumwun  33619  cyc3genpm  33695  elrgspnlem4  33788  erler  33808  rlocaddval  33812  rlocmulval  33813  rloccring  33814  rhmquskerlem  33957  elrspunidl  33960  rhmimaidl  33964  mxidlirredi  33978  mxidlirred  33979  ssmxidllem  33980  qsdrngi  34001  dflringlem2  34009  1arithidom  34051  1arithufdlem3  34060  r1plmhm  34123  r1pquslmic  34124  lbsdiflsp0  34240  dimkerim  34241  fedgmul  34245  fldextrspunlsplem  34287  fldext2chn  34342  constrextdg2lem  34362  txomap  34448  heicant  38541  mblfinlem3  38545  primrootscoprmpow  43117  aks6d1c2lem4  43145  aks6d1c5  43157  limclner  46605  hoidmvle  47554  chnerlem1  47836