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 482 . 2 ((𝜑𝜒) → 𝜓)
32ad7antr 736 1 (((((((((𝜑𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 398
This theorem is referenced by:  ad9antr  740  ad9antlr  741  simp-8l  789  legso  27001  miriso  27072  midexlem  27094  opphl  27156  trgcopy  27206  inaghl  27247  cyc3conja  31465  lbsdiflsp0  31748  dimkerim  31749  fedgmul  31753  qtophaus  31827  zarcmplem  31872  afsval  32692  dffltz  40507  hoidmvle  44187  smfmullem3  44380
  Copyright terms: Public domain W3C validator