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  28607  miriso  28678  midexlem  28700  opphl  28762  trgcopy  28812  inaghl  28853  cyc3conja  33177  elrgspnlem4  33249  rloccring  33274  ssdifidlprm  33486  mxidlirred  33500  qsdrngi  33523  1arithidom  33565  1arithufdlem3  33574  lbsdiflsp0  33677  dimkerim  33678  fedgmul  33682  constrelextdg2  33788  qtophaus  33835  zarcmplem  33880  afsval  34686  dffltz  42644  hoidmvle  46615  smfmullem3  46808
  Copyright terms: Public domain W3C validator