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

Theorem ad8antr 739
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 737 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  741  ad9antlr  742  simp-8l  790  legso  28625  miriso  28696  midexlem  28718  opphl  28780  trgcopy  28830  inaghl  28871  cyc3conja  33150  rloccring  33242  ssdifidlprm  33451  mxidlirred  33465  qsdrngi  33488  1arithidom  33530  1arithufdlem3  33539  lbsdiflsp0  33639  dimkerim  33640  fedgmul  33644  constrelextdg2  33737  qtophaus  33782  zarcmplem  33827  afsval  34648  dffltz  42589  hoidmvle  46521  smfmullem3  46714
  Copyright terms: Public domain W3C validator