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 481	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
3	2	ad4antr 730	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  734  ad6antlr  735  simp-5l  783  fimaproj  8072  catass  17580  catpropd  17603  cidpropd  17604  monpropd  17634  funcpropd  17801  fucpropd  17880  drsdirfi  18208  mhmmnd  18883  neitr  22568  xkoccn  23007  trust  23618  restutopopn  23627  ucncn  23674  trcfilu  23683  ulmcau  25791  lgamucov  26424  tgcgrxfr  27523  tgbtwnconn1  27580  legov  27590  legso  27604  midexlem  27697  perpneq  27719  footexALT  27723  footex  27726  colperpexlem3  27737  colperpex  27738  opphllem  27740  opphllem3  27754  outpasch  27760  hlpasch  27761  lmieu  27789  trgcopy  27809  trgcopyeu  27811  dfcgra2  27835  acopyeu  27839  cgrg3col4  27858  f1otrg  27876  fnpreimac  31654  nn0xmulclb  31744  s3f1  31873  omndmul2  31990  cyc3conja  32076  nsgqusf1olem3  32267  ghmqusker  32272  rhmqusker  32278  rhmimaidl  32282  mxidlprm  32313  ssmxidllem  32314  fedgmul  32413  extdg1id  32439  qtophaus  32506  locfinreflem  32510  zarclssn  32543  hgt750lemb  33358  matunitlindflem1  36147  heicant  36186  mblfinlem3  36190  mblfinlem4  36191  itg2gt0cn  36206  sstotbnd2  36306  aks4d1p8  40617  aks6d1c2p2  40622  fsuppind  40823  pell1234qrdich  41242  omabs2  41725  supxrgelem  43692  icccncfext  44248  etransclem35  44630  smflimlem2  45133