Theorem ad5antr 732

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  ad6antr  734  ad6antlr  735  simp-5l  783  fimaproj  7822  catass  16952  catpropd  16974  cidpropd  16975  monpropd  17002  funcpropd  17165  fucpropd  17242  drsdirfi  17543  mhmmnd  18216  neitr  21783  xkoccn  22222  trust  22833  restutopopn  22842  ucncn  22889  trcfilu  22898  ulmcau  24981  lgamucov  25613  tgcgrxfr  26302  tgbtwnconn1  26359  legov  26369  legso  26383  midexlem  26476  perpneq  26498  footexALT  26502  footex  26505  colperpexlem3  26516  colperpex  26517  opphllem  26519  opphllem3  26533  outpasch  26539  hlpasch  26540  lmieu  26568  trgcopy  26588  trgcopyeu  26590  dfcgra2  26614  acopyeu  26618  cgrg3col4  26637  f1otrg  26655  fnpreimac  30416  nn0xmulclb  30496  s3f1  30623  omndmul2  30734  cyc3conja  30820  mxidlprm  31001  ssmxidllem  31002  fedgmul  31051  extdg1id  31077  qtophaus  31124  locfinreflem  31128  hgt750lemb  31948  matunitlindflem1  34923  heicant  34962  mblfinlem3  34966  mblfinlem4  34967  itg2gt0cn  34982  sstotbnd2  35085  pell1234qrdich  39534  supxrgelem  41679  icccncfext  42244  etransclem35  42628  smflimlem2  43122