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  17780  funcpropd  17997  natpropd  18074  ghmqusnsg  19415  ghmquskerlem3  19419  rhmqusnsg  21494  ssdifidllem  21553  ssdifidlprm  21555  matunitlindflem1  22907  restutop  24469  utopreg  24484  restmetu  24802  lgamucov  27282  istrkgcb  28805  tgsegconeu  28836  tgifscgr  28858  tgbtwnconn1lem3  28924  legtrd  28939  miriso  29029  footexALT  29080  footex  29083  opphllem3  29112  opphl  29117  plng3p  29162  trgcopy  29198  cgratr  29217  zerocgra  29218  dfcgra2  29225  ragcgra  29230  ragsupplcgra  29232  tgaaddcpbllem1  29236  inaghl  29251  cgrg3col4  29259  cgraer  29264  angmgmaddeu1  29266  angmgmaddcpbl  29277  angmgmaddcl  29278  angmgmaddlid  29279  prlngmolem2  29318  f1otrge  29336  clwlkclwwlklem2  30478  gsumwun  33524  cyc3genpm  33600  elrgspnlem4  33693  erler  33713  rlocaddval  33717  rlocmulval  33718  rloccring  33719  rhmquskerlem  33861  elrspunidl  33864  rhmimaidl  33868  mxidlirredi  33882  mxidlirred  33883  ssmxidllem  33884  qsdrngi  33905  dflringlem2  33913  1arithidom  33955  1arithufdlem3  33964  r1plmhm  34027  r1pquslmic  34028  lbsdiflsp0  34144  dimkerim  34145  fedgmul  34149  fldextrspunlsplem  34191  fldext2chn  34246  constrextdg2lem  34266  txomap  34352  heicant  38412  mblfinlem3  38416  primrootscoprmpow  42973  aks6d1c2lem4  43001  aks6d1c5  43013  limclner  46487  hoidmvle  47436  chnerlem1  47718