Theorem ad5antr 773

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 769	1 ⊢ ((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 383

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 197  df-an 385

This theorem is referenced by:  ad6antr  777  ad6antrOLD  778  ad6antlr  779  catass  16394  catpropd  16416  cidpropd  16417  monpropd  16444  funcpropd  16607  fucpropd  16684  drsdirfi  16985  mhmmnd  17584  neitr  21032  xkoccn  21470  trust  22080  restutopopn  22089  ucncn  22136  trcfilu  22145  ulmcau  24194  lgamucov  24809  tgcgrxfr  25458  tgbtwnconn1  25515  legov  25525  legso  25539  midexlem  25632  perpneq  25654  footex  25658  colperpexlem3  25669  colperpex  25670  opphllem  25672  opphllem3  25686  outpasch  25692  hlpasch  25693  lmieu  25721  trgcopy  25741  trgcopyeu  25743  dfcgra2  25766  acopyeu  25770  cgrg3col4  25779  f1otrg  25796  omndmul2  29840  fimaproj  30028  qtophaus  30031  locfinreflem  30035  hgt750lemb  30862  matunitlindflem1  33535  heicant  33574  mblfinlem3  33578  mblfinlem4  33579  itg2gt0cn  33595  sstotbnd2  33703  pell1234qrdich  37742  supxrgelem  39866  icccncfext  40418  etransclem35  40804  smflimlem2  41301