Theorem ad5antr 735

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  ad6antr  737  ad6antlr  738  simp-5l  785  fimaproj  8078  catass  17643  catpropd  17666  cidpropd  17667  monpropd  17695  funcpropd  17860  fucpropd  17938  drsdirfi  18262  chnind  18578  mhmmnd  19031  ghmqusnsg  19248  ghmquskerlem3  19252  omndmul2  20099  rhmqusnsg  21275  neitr  23155  xkoccn  23594  trust  24204  restutopopn  24213  ucncn  24259  trcfilu  24268  ulmcau  26373  lgamucov  27015  tgcgrxfr  28600  tgbtwnconn1  28657  legov  28667  legso  28681  midexlem  28774  perpneq  28796  footexALT  28800  footex  28803  colperpexlem3  28814  colperpex  28815  opphllem  28817  opphllem3  28831  outpasch  28837  hlpasch  28838  lmieu  28866  trgcopy  28886  trgcopyeu  28888  dfcgra2  28912  acopyeu  28916  cgrg3col4  28935  f1otrg  28953  fnpreimac  32758  nn0xmulclb  32859  s3f1  33022  ccatws1f1o  33026  mndlactf1o  33105  gsumwun  33152  gsumwrd2dccatlem  33153  cyc3conja  33233  elrgspnlem4  33321  erler  33341  rlocf1  33349  isdrng4  33371  fracfld  33384  dvdsruasso  33460  nsgqusf1olem3  33490  rhmquskerlem  33500  elrspunsn  33504  rhmimaidl  33507  ssdifidllem  33531  ssdifidlprm  33533  mxidlprm  33545  ssmxidllem  33548  qsdrng  33572  rprmasso2  33601  1arithufdlem3  33621  1arithufdlem4  33622  dfufd2lem  33624  mplvrpmrhm  33706  esplyfval1  33732  esplyind  33734  vieta  33739  fedgmul  33791  extdg1id  33826  constrextdg2lem  33908  qtophaus  33996  locfinreflem  34000  zarclssn  34033  hgt750lemb  34816  matunitlindflem1  37951  heicant  37990  mblfinlem3  37994  mblfinlem4  37995  itg2gt0cn  38010  sstotbnd2  38109  aks4d1p8  42540  aks6d1c2p2  42572  aks6d1c2  42583  aks6d1c6lem3  42625  unitscyglem3  42650  fsuppind  43037  pell1234qrdich  43307  omabs2  43778  supxrgelem  45785  icccncfext  46333  etransclem35  46715  smflimlem2  47218  uppropd  49668  fuco21  49823