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  17892  funcpropd  18109  natpropd  18186  ghmqusnsg  19529  ghmquskerlem3  19533  rhmqusnsg  21614  ssdifidllem  21673  ssdifidlprm  21675  matunitlindflem1  23027  restutop  24589  utopreg  24604  restmetu  24922  lgamucov  27398  istrkgcb  28951  tgsegconeu  28982  tgifscgr  29004  tgbtwnconn1lem3  29070  legtrd  29085  miriso  29175  footexALT  29226  footex  29229  opphllem3  29258  opphl  29263  plng3p  29308  trgcopy  29344  cgratr  29363  zerocgra  29364  dfcgra2  29371  ragcgra  29376  ragsupplcgra  29378  tgaaddcpbllem1  29382  inaghl  29397  cgrg3col4  29405  cgraer  29410  angmgmaddeu1  29412  angmgmaddcpbl  29423  angmgmaddcl  29424  angmgmaddlid  29425  prlngmolem2  29464  f1otrge  29482  clwlkclwwlklem2  30624  gsumwun  33713  cyc3genpm  33789  elrgspnlem4  33882  erler  33902  rlocaddval  33906  rlocmulval  33907  rloccring  33908  edompidlem  33940  rhmquskerlem  34059  elrspunidl  34062  rhmimaidl  34066  mxidlirredi  34080  mxidlirred  34081  ssmxidllem  34082  qsdrngi  34103  dflringlem2  34111  1arithidom  34153  1arithufdlem3  34162  r1plmhm  34224  r1pquslmic  34225  lbsdiflsp0  34341  dimkerim  34342  fedgmul  34346  fldextrspunlsplem  34388  fldext2chn  34443  constrextdg2lem  34463  txomap  34549  heicant  38778  mblfinlem3  38782  primrootscoprmpow  43352  aks6d1c2lem4  43380  aks6d1c5  43392  limclner  46876  hoidmvle  47825  chnerlem1  48107