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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  ad6antr  732  ad6antlr  733  simp-5l  781  catass  16790  catpropd  16812  cidpropd  16813  monpropd  16840  funcpropd  17003  fucpropd  17080  drsdirfi  17381  mhmmnd  17982  neitr  21476  xkoccn  21915  trust  22525  restutopopn  22534  ucncn  22581  trcfilu  22590  ulmcau  24670  lgamucov  25301  tgcgrxfr  25990  tgbtwnconn1  26047  legov  26057  legso  26071  midexlem  26164  perpneq  26186  footexALT  26190  footex  26193  colperpexlem3  26204  colperpex  26205  opphllem  26207  opphllem3  26221  outpasch  26227  hlpasch  26228  lmieu  26256  trgcopy  26276  trgcopyeu  26278  dfcgra2  26302  acopyeu  26307  cgrg3col4  26326  f1otrg  26344  fnpreimac  30102  nn0xmulclb  30180  s3f1  30299  omndmul2  30369  cyc3conja  30433  fedgmul  30627  extdg1id  30653  fimaproj  30710  qtophaus  30713  locfinreflem  30717  hgt750lemb  31540  matunitlindflem1  34440  heicant  34479  mblfinlem3  34483  mblfinlem4  34484  itg2gt0cn  34499  sstotbnd2  34605  pell1234qrdich  38964  supxrgelem  41167  icccncfext  41733  etransclem35  42118  smflimlem2  42612