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

Syntax hints:   → wi 4   ∧ wa 395

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 396

This theorem is referenced by:  ad6antr  732  ad6antlr  733  simp-5l  781  fimaproj  7947  catass  17312  catpropd  17335  cidpropd  17336  monpropd  17366  funcpropd  17532  fucpropd  17611  drsdirfi  17938  mhmmnd  18612  neitr  22239  xkoccn  22678  trust  23289  restutopopn  23298  ucncn  23345  trcfilu  23354  ulmcau  25459  lgamucov  26092  tgcgrxfr  26783  tgbtwnconn1  26840  legov  26850  legso  26864  midexlem  26957  perpneq  26979  footexALT  26983  footex  26986  colperpexlem3  26997  colperpex  26998  opphllem  27000  opphllem3  27014  outpasch  27020  hlpasch  27021  lmieu  27049  trgcopy  27069  trgcopyeu  27071  dfcgra2  27095  acopyeu  27099  cgrg3col4  27118  f1otrg  27136  fnpreimac  30910  nn0xmulclb  30996  s3f1  31123  omndmul2  31240  cyc3conja  31326  nsgqusf1olem3  31502  rhmimaidl  31511  mxidlprm  31542  ssmxidllem  31543  fedgmul  31614  extdg1id  31640  qtophaus  31688  locfinreflem  31692  zarclssn  31725  hgt750lemb  32536  matunitlindflem1  35700  heicant  35739  mblfinlem3  35743  mblfinlem4  35744  itg2gt0cn  35759  sstotbnd2  35859  aks4d1p8  40023  fsuppind  40202  pell1234qrdich  40599  supxrgelem  42766  icccncfext  43318  etransclem35  43700  smflimlem2  44194