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

Theorem ad8antr 740
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 480 . 2 ((𝜑𝜒) → 𝜓)
32ad7antr 738 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 207  df-an 396
This theorem is referenced by:  ad9antr  742  ad9antlr  743  simp-8l  791  legso  28621  miriso  28692  midexlem  28714  opphl  28776  trgcopy  28826  inaghl  28867  cyc3conja  33159  elrgspnlem4  33234  rloccring  33256  ssdifidlprm  33465  mxidlirred  33479  qsdrngi  33502  1arithidom  33544  1arithufdlem3  33553  lbsdiflsp0  33653  dimkerim  33654  fedgmul  33658  constrelextdg2  33751  qtophaus  33796  zarcmplem  33841  afsval  34664  dffltz  42620  hoidmvle  46555  smfmullem3  46748
  Copyright terms: Public domain W3C validator