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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  ad6antr  734  ad6antlr  735  simp-5l  783  fimaproj  7831  catass  16959  catpropd  16981  cidpropd  16982  monpropd  17009  funcpropd  17172  fucpropd  17249  drsdirfi  17550  mhmmnd  18223  neitr  21790  xkoccn  22229  trust  22840  restutopopn  22849  ucncn  22896  trcfilu  22905  ulmcau  24985  lgamucov  25617  tgcgrxfr  26306  tgbtwnconn1  26363  legov  26373  legso  26387  midexlem  26480  perpneq  26502  footexALT  26506  footex  26509  colperpexlem3  26520  colperpex  26521  opphllem  26523  opphllem3  26537  outpasch  26543  hlpasch  26544  lmieu  26572  trgcopy  26592  trgcopyeu  26594  dfcgra2  26618  acopyeu  26622  cgrg3col4  26641  f1otrg  26659  fnpreimac  30418  nn0xmulclb  30498  s3f1  30625  omndmul2  30715  cyc3conja  30801  mxidlprm  30979  ssmxidllem  30980  fedgmul  31029  extdg1id  31055  qtophaus  31102  locfinreflem  31106  hgt750lemb  31929  matunitlindflem1  34890  heicant  34929  mblfinlem3  34933  mblfinlem4  34934  itg2gt0cn  34949  sstotbnd2  35054  pell1234qrdich  39465  supxrgelem  41612  icccncfext  42177  etransclem35  42561  smflimlem2  43055