Theorem ad5antr 730

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

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  ad6antr  732  ad6antlr  733  simp-5l  781  fimaproj  8123  catass  17634  catpropd  17657  cidpropd  17658  monpropd  17688  funcpropd  17855  fucpropd  17934  drsdirfi  18262  mhmmnd  18983  neitr  22904  xkoccn  23343  trust  23954  restutopopn  23963  ucncn  24010  trcfilu  24019  ulmcau  26143  lgamucov  26778  tgcgrxfr  28036  tgbtwnconn1  28093  legov  28103  legso  28117  midexlem  28210  perpneq  28232  footexALT  28236  footex  28239  colperpexlem3  28250  colperpex  28251  opphllem  28253  opphllem3  28267  outpasch  28273  hlpasch  28274  lmieu  28302  trgcopy  28322  trgcopyeu  28324  dfcgra2  28348  acopyeu  28352  cgrg3col4  28371  f1otrg  28389  fnpreimac  32163  nn0xmulclb  32251  s3f1  32380  omndmul2  32500  cyc3conja  32586  isdrng4  32665  dvdsruasso  32764  nsgqusf1olem3  32800  ghmquskerlem3  32805  rhmquskerlem  32817  elrspunsn  32821  rhmimaidl  32824  mxidlprm  32860  ssmxidllem  32863  qsdrng  32885  fedgmul  33004  extdg1id  33030  qtophaus  33114  locfinreflem  33118  zarclssn  33151  hgt750lemb  33966  matunitlindflem1  36787  heicant  36826  mblfinlem3  36830  mblfinlem4  36831  itg2gt0cn  36846  sstotbnd2  36945  aks4d1p8  41258  aks6d1c2p2  41263  fsuppind  41464  pell1234qrdich  41901  omabs2  42384  supxrgelem  44345  icccncfext  44901  etransclem35  45283  smflimlem2  45786