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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  ad6antr  736  ad6antlr  737  simp-5l  785  fimaproj  7902  catass  17189  catpropd  17212  cidpropd  17213  monpropd  17242  funcpropd  17407  fucpropd  17486  drsdirfi  17812  mhmmnd  18485  neitr  22077  xkoccn  22516  trust  23127  restutopopn  23136  ucncn  23182  trcfilu  23191  ulmcau  25287  lgamucov  25920  tgcgrxfr  26609  tgbtwnconn1  26666  legov  26676  legso  26690  midexlem  26783  perpneq  26805  footexALT  26809  footex  26812  colperpexlem3  26823  colperpex  26824  opphllem  26826  opphllem3  26840  outpasch  26846  hlpasch  26847  lmieu  26875  trgcopy  26895  trgcopyeu  26897  dfcgra2  26921  acopyeu  26925  cgrg3col4  26944  f1otrg  26962  fnpreimac  30728  nn0xmulclb  30814  s3f1  30941  omndmul2  31057  cyc3conja  31143  nsgqusf1olem3  31314  rhmimaidl  31323  mxidlprm  31354  ssmxidllem  31355  fedgmul  31426  extdg1id  31452  qtophaus  31500  locfinreflem  31504  zarclssn  31537  hgt750lemb  32348  matunitlindflem1  35510  heicant  35549  mblfinlem3  35553  mblfinlem4  35554  itg2gt0cn  35569  sstotbnd2  35669  fsuppind  39989  pell1234qrdich  40386  supxrgelem  42549  icccncfext  43103  etransclem35  43485  smflimlem2  43979