Theorem ad5antr 747

Description: Deduction adding 5 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
ad5antr	⊢ ((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)

Proof of Theorem ad5antr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	adantr 486	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
3	2	ad4antr 745	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:  ad6antr  749  ad6antlr  750  simp-5l  797  fimaproj  8136  catass  17840  catpropd  17863  cidpropd  17864  monpropd  17892  funcpropd  18057  fucpropd  18135  drsdirfi  18459  chnind  18775  mhmmnd  19254  ghmqusnsg  19476  ghmquskerlem3  19480  omndmul2  20327  isdrng4  20972  rhmqusnsg  21561  ssdifidllem  21620  ssdifidlprm  21622  matunitlindflem1  22974  neitr  23478  xkoccn  23918  trust  24528  restutopopn  24537  ucncn  24583  trcfilu  24592  ulmcau  26704  lgamucov  27347  tgcgrxfr  28963  tgbtwnconn1  29020  legov  29030  legso  29044  tglnpt3  29104  tglnpt4  29105  midexlem  29146  perpneq  29171  footexALT  29175  footex  29178  colperpexlem3  29190  colperpex  29191  opphllem  29193  opphllem3  29207  outpasch  29215  hlpasch  29216  lnssplng  29252  lmieu  29271  trgcopy  29293  trgcopyeu  29295  dfcgra2  29320  acopyeu  29324  cgrarag  29326  tgaaddcpbl  29334  cgrg3col4  29354  angmgmaddeu1  29361  angmgmaddov2lem  29369  angmgmaddcpbl  29372  perpprlng  29410  prlngex  29411  prlngmolem1  29412  prlngmolem2  29413  prlngmo2  29416  quadcgrprlng  29426  f1otrg  29430  fnpreimac  33246  nn0xmulclb  33345  s3f1  33493  ccatws1f1o  33496  mndlactf1o  33573  gsumwun  33619  gsumwrd2dccatlem  33620  cyc3conja  33700  elrgspnlem4  33788  erler  33808  rlocf1  33817  rlocisunit  33819  fracfld  33852  dvdsruasso  33922  nsgqusf1olem3  33948  rhmquskerlem  33957  elrspunsn  33961  rhmimaidl  33964  mxidlprm  33977  ssmxidllem  33980  qsdrng  34003  rprmasso2  34040  1arithufdlem3  34060  1arithufdlem4  34061  dfufd2lem  34063  mplvrpmrhm  34161  esplyfval1  34187  esplyind  34189  vieta  34194  fedgmul  34245  extdg1id  34280  constrextdg2lem  34362  qtophaus  34450  locfinreflem  34454  zarclssn  34487  hgt750lemb  35268  heicant  38541  mblfinlem3  38545  mblfinlem4  38546  itg2gt0cn  38561  sstotbnd2  38676  aks4d1p8  43105  aks6d1c2p2  43137  aks6d1c2  43148  aks6d1c6lem3  43190  unitscyglem3  43215  fsuppind  43580  pell1234qrdich  43821  omabs2  44292  supxrgelem  46293  icccncfext  46841  etransclem35  47223  smflimlem2  47726  uppropd  50233  fuco21  50388