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

Theorem ad5antlr 733
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 482 . 2 ((𝜒𝜑) → 𝜓)
32ad4antr 730 1 ((((((𝜒𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)
Colors of variables: wff setvar class
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:  simp-5r  784  fimaproj  8123  restmetu  24086  foresf1o  31780  2ndresdju  31912  nn0xmulclb  32022  isdrng4  32436  elrspunidl  32591  elrspunsn  32592  rhmpreimaprmidl  32615  fedgmul  32775  locfinreflem  32889  pstmxmet  32946  satfdmlem  34428  mblfinlem3  36613  itg2gt0cn  36629  dffltz  41458  pell1234qrmulcl  41675  suplesup  44128  limclner  44446  bgoldbtbnd  46556  isomushgr  46573
  Copyright terms: Public domain W3C validator