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

Theorem ad8antr 738
Description: Deduction adding 8 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
ad8antr (((((((((𝜑𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) → 𝜓)

Proof of Theorem ad8antr
StepHypRef Expression
1 ad2ant.1 . . 3 (𝜑𝜓)
21adantr 481 . 2 ((𝜑𝜒) → 𝜓)
32ad7antr 736 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:  ad9antr  740  ad9antlr  741  simp-8l  789  legso  27488  miriso  27559  midexlem  27581  opphl  27643  trgcopy  27693  inaghl  27734  cyc3conja  31950  lbsdiflsp0  32261  dimkerim  32262  fedgmul  32266  qtophaus  32357  zarcmplem  32402  afsval  33224  dffltz  40949  hoidmvle  44812  smfmullem3  45005
  Copyright terms: Public domain W3C validator