Theorem ad5antr 746

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 485	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
3	2	ad4antr 744	1 ⊢ ((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 400

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 401

This theorem is referenced by:  ad6antr  748  ad6antlr  749  simp-5l  796  fimaproj  8119  catass  17732  catpropd  17755  cidpropd  17756  monpropd  17784  funcpropd  17949  fucpropd  18027  drsdirfi  18351  chnind  18667  mhmmnd  19121  ghmqusnsg  19343  ghmquskerlem3  19347  omndmul2  20194  rhmqusnsg  21387  ssdifidllem  21444  ssdifidlprm  21446  neitr  23298  xkoccn  23737  trust  24347  restutopopn  24356  ucncn  24402  trcfilu  24411  ulmcau  26516  lgamucov  27160  tgcgrxfr  28745  tgbtwnconn1  28802  legov  28812  legso  28826  tglnpt3  28881  tglnpt4  28882  midexlem  28923  perpneq  28945  footexALT  28949  footex  28952  colperpexlem3  28963  colperpex  28964  opphllem  28966  opphllem3  28980  outpasch  28986  hlpasch  28987  lnssplng  29022  lmieu  29036  trgcopy  29056  trgcopyeu  29058  dfcgra2  29082  acopyeu  29086  cgrg3col4  29105  f1otrg  29129  fnpreimac  32927  nn0xmulclb  33028  s3f1  33180  ccatws1f1o  33184  mndlactf1o  33263  gsumwun  33309  gsumwrd2dccatlem  33310  cyc3conja  33390  elrgspnlem4  33478  erler  33498  rlocf1  33507  rlocisunit  33509  isdrng4  33531  fracfld  33544  dvdsruasso  33614  nsgqusf1olem3  33640  rhmquskerlem  33649  elrspunsn  33653  rhmimaidl  33656  mxidlprm  33670  ssmxidllem  33673  qsdrng  33696  rprmasso2  33733  1arithufdlem3  33753  1arithufdlem4  33754  dfufd2lem  33756  mplvrpmrhm  33854  esplyfval1  33880  esplyind  33882  vieta  33887  fedgmul  33938  extdg1id  33973  constrextdg2lem  34055  qtophaus  34143  locfinreflem  34147  zarclssn  34180  hgt750lemb  34960  matunitlindflem1  38127  heicant  38166  mblfinlem3  38170  mblfinlem4  38171  itg2gt0cn  38186  sstotbnd2  38285  aks4d1p8  42716  aks6d1c2p2  42748  aks6d1c2  42759  aks6d1c6lem3  42801  unitscyglem3  42826  fsuppind  43184  pell1234qrdich  43450  omabs2  43921  supxrgelem  45911  icccncfext  46459  etransclem35  46841  smflimlem2  47344  uppropd  49810  fuco21  49965