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  8182  catass  17892  catpropd  17915  cidpropd  17916  monpropd  17944  funcpropd  18109  fucpropd  18187  drsdirfi  18511  chnind  18827  mhmmnd  19306  ghmqusnsg  19529  ghmquskerlem3  19533  omndmul2  20380  isdrng4  21025  rhmqusnsg  21614  ssdifidllem  21673  ssdifidlprm  21675  matunitlindflem1  23027  neitr  23531  xkoccn  23971  trust  24581  restutopopn  24590  ucncn  24636  trcfilu  24645  ulmcau  26755  lgamucov  27398  tgcgrxfr  29014  tgbtwnconn1  29071  legov  29081  legso  29095  tglnpt3  29155  tglnpt4  29156  midexlem  29197  perpneq  29222  footexALT  29226  footex  29229  colperpexlem3  29241  colperpex  29242  opphllem  29244  opphllem3  29258  outpasch  29266  hlpasch  29267  lnssplng  29303  lmieu  29322  trgcopy  29344  trgcopyeu  29346  dfcgra2  29371  acopyeu  29375  cgrarag  29377  tgaaddcpbl  29385  cgrg3col4  29405  angmgmaddeu1  29412  angmgmaddov2lem  29420  angmgmaddcpbl  29423  perpprlng  29461  prlngex  29462  prlngmolem1  29463  prlngmolem2  29464  prlngmo2  29467  quadcgrprlng  29477  f1otrg  29481  fnpreimac  33339  nn0xmulclb  33436  s3f1  33584  ccatws1f1o  33587  mndlactf1o  33667  gsumwun  33713  gsumwrd2dccatlem  33714  cyc3conja  33794  elrgspnlem4  33882  erler  33902  rlocf1  33911  rlocisunit  33913  zzedom  33939  edompidlem  33940  fracfld  33954  dvdsruasso  34024  nsgqusf1olem3  34050  rhmquskerlem  34059  elrspunsn  34063  rhmimaidl  34066  mxidlprm  34079  ssmxidllem  34082  qsdrng  34105  rprmasso2  34142  1arithufdlem3  34162  1arithufdlem4  34163  dfufd2lem  34165  mplvrpmrhm  34262  esplyfval1  34288  esplyind  34290  vieta  34295  fedgmul  34346  extdg1id  34381  constrextdg2lem  34463  qtophaus  34551  locfinreflem  34555  zarclssn  34588  hgt750lemb  35368  heicant  38778  mblfinlem3  38782  mblfinlem4  38783  itg2gt0cn  38798  sstotbnd2  38911  aks4d1p8  43340  aks6d1c2p2  43372  aks6d1c2  43383  aks6d1c6lem3  43425  unitscyglem3  43450  fsuppind  43822  pell1234qrdich  44072  omabs2  44537  supxrgelem  46564  icccncfext  47112  etransclem35  47494  smflimlem2  47997  uppropd  50512  fuco21  50673