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  784  fimaproj  8074  catass  17602  catpropd  17625  cidpropd  17626  monpropd  17654  funcpropd  17819  fucpropd  17897  drsdirfi  18221  chnind  18537  mhmmnd  18987  ghmqusnsg  19204  ghmquskerlem3  19208  omndmul2  20055  rhmqusnsg  21232  neitr  23105  xkoccn  23544  trust  24154  restutopopn  24163  ucncn  24209  trcfilu  24218  ulmcau  26341  lgamucov  26985  tgcgrxfr  28506  tgbtwnconn1  28563  legov  28573  legso  28587  midexlem  28680  perpneq  28702  footexALT  28706  footex  28709  colperpexlem3  28720  colperpex  28721  opphllem  28723  opphllem3  28737  outpasch  28743  hlpasch  28744  lmieu  28772  trgcopy  28792  trgcopyeu  28794  dfcgra2  28818  acopyeu  28822  cgrg3col4  28841  f1otrg  28859  fnpreimac  32664  nn0xmulclb  32765  s3f1  32939  ccatws1f1o  32943  mndlactf1o  33022  gsumwun  33056  gsumwrd2dccatlem  33057  cyc3conja  33137  elrgspnlem4  33223  erler  33243  rlocf1  33251  isdrng4  33272  fracfld  33285  dvdsruasso  33361  nsgqusf1olem3  33391  rhmquskerlem  33401  elrspunsn  33405  rhmimaidl  33408  ssdifidllem  33432  ssdifidlprm  33434  mxidlprm  33446  ssmxidllem  33449  qsdrng  33473  rprmasso2  33502  1arithufdlem3  33522  1arithufdlem4  33523  dfufd2lem  33525  mplvrpmrhm  33588  fedgmul  33655  extdg1id  33690  constrextdg2lem  33772  qtophaus  33860  locfinreflem  33864  zarclssn  33897  hgt750lemb  34680  matunitlindflem1  37666  heicant  37705  mblfinlem3  37709  mblfinlem4  37710  itg2gt0cn  37725  sstotbnd2  37824  aks4d1p8  42190  aks6d1c2p2  42222  aks6d1c2  42233  aks6d1c6lem3  42275  unitscyglem3  42300  fsuppind  42698  pell1234qrdich  42968  omabs2  43439  supxrgelem  45450  icccncfext  45999  etransclem35  46381  smflimlem2  46884  uppropd  49296  fuco21  49451