Theorem ad5antr 731

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 729	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 206  df-an 397

This theorem is referenced by:  ad6antr  733  ad6antlr  734  simp-5l  782  fimaproj  7976  catass  17395  catpropd  17418  cidpropd  17419  monpropd  17449  funcpropd  17616  fucpropd  17695  drsdirfi  18023  mhmmnd  18697  neitr  22331  xkoccn  22770  trust  23381  restutopopn  23390  ucncn  23437  trcfilu  23446  ulmcau  25554  lgamucov  26187  tgcgrxfr  26879  tgbtwnconn1  26936  legov  26946  legso  26960  midexlem  27053  perpneq  27075  footexALT  27079  footex  27082  colperpexlem3  27093  colperpex  27094  opphllem  27096  opphllem3  27110  outpasch  27116  hlpasch  27117  lmieu  27145  trgcopy  27165  trgcopyeu  27167  dfcgra2  27191  acopyeu  27195  cgrg3col4  27214  f1otrg  27232  fnpreimac  31008  nn0xmulclb  31094  s3f1  31221  omndmul2  31338  cyc3conja  31424  nsgqusf1olem3  31600  rhmimaidl  31609  mxidlprm  31640  ssmxidllem  31641  fedgmul  31712  extdg1id  31738  qtophaus  31786  locfinreflem  31790  zarclssn  31823  hgt750lemb  32636  matunitlindflem1  35773  heicant  35812  mblfinlem3  35816  mblfinlem4  35817  itg2gt0cn  35832  sstotbnd2  35932  aks4d1p8  40095  fsuppind  40279  pell1234qrdich  40683  supxrgelem  42876  icccncfext  43428  etransclem35  43810  smflimlem2  44307