MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ad5antlr Structured version   Visualization version   GIF version

Theorem ad5antlr 734
Description: Deduction adding 5 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.)
Hypothesis
Ref Expression
ad2ant.1 (𝜑𝜓)
Assertion
Ref Expression
ad5antlr ((((((𝜒𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)

Proof of Theorem ad5antlr
StepHypRef Expression
1 ad2ant.1 . . 3 (𝜑𝜓)
21adantl 481 . 2 ((𝜒𝜑) → 𝜓)
32ad4antr 731 1 ((((((𝜒𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)
Colors of variables: wff setvar class
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:  simp-5r  785  fimaproj  8134  restmetu  24466  foresf1o  32286  2ndresdju  32418  nn0xmulclb  32525  isdrng4  32932  elrspunidl  33079  elrspunsn  33080  rhmpreimaprmidl  33103  fedgmul  33261  locfinreflem  33377  pstmxmet  33434  satfdmlem  34914  mblfinlem3  37067  itg2gt0cn  37083  dffltz  41980  pell1234qrmulcl  42197  suplesup  44644  limclner  44962  bgoldbtbnd  47072  gricushgr  47106
  Copyright terms: Public domain W3C validator