Theorem ad5antr 734

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 732	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  736  ad6antlr  737  simp-5l  785  fimaproj  8160  catass  17729  catpropd  17752  cidpropd  17753  monpropd  17781  funcpropd  17947  fucpropd  18025  drsdirfi  18351  mhmmnd  19082  ghmqusnsg  19300  ghmquskerlem3  19304  rhmqusnsg  21295  neitr  23188  xkoccn  23627  trust  24238  restutopopn  24247  ucncn  24294  trcfilu  24303  ulmcau  26438  lgamucov  27081  tgcgrxfr  28526  tgbtwnconn1  28583  legov  28593  legso  28607  midexlem  28700  perpneq  28722  footexALT  28726  footex  28729  colperpexlem3  28740  colperpex  28741  opphllem  28743  opphllem3  28757  outpasch  28763  hlpasch  28764  lmieu  28792  trgcopy  28812  trgcopyeu  28814  dfcgra2  28838  acopyeu  28842  cgrg3col4  28861  f1otrg  28879  fnpreimac  32681  nn0xmulclb  32775  s3f1  32931  ccatws1f1o  32936  chnind  33001  mndlactf1o  33035  gsumwun  33068  gsumwrd2dccatlem  33069  omndmul2  33089  cyc3conja  33177  elrgspnlem4  33249  erler  33269  rlocf1  33277  isdrng4  33298  fracfld  33310  dvdsruasso  33413  nsgqusf1olem3  33443  rhmquskerlem  33453  elrspunsn  33457  rhmimaidl  33460  ssdifidllem  33484  ssdifidlprm  33486  mxidlprm  33498  ssmxidllem  33501  qsdrng  33525  rprmasso2  33554  1arithufdlem3  33574  1arithufdlem4  33575  dfufd2lem  33577  fedgmul  33682  extdg1id  33716  constrextdg2lem  33789  qtophaus  33835  locfinreflem  33839  zarclssn  33872  hgt750lemb  34671  matunitlindflem1  37623  heicant  37662  mblfinlem3  37666  mblfinlem4  37667  itg2gt0cn  37682  sstotbnd2  37781  aks4d1p8  42088  aks6d1c2p2  42120  aks6d1c2  42131  aks6d1c6lem3  42173  unitscyglem3  42198  fsuppind  42600  pell1234qrdich  42872  omabs2  43345  supxrgelem  45348  icccncfext  45902  etransclem35  46284  smflimlem2  46787  fuco21  49031