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

Theorem ad6antr 767
Description: Deduction adding 6 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.)
Hypothesis
Ref Expression
ad2ant.1 (𝜑𝜓)
Assertion
Ref Expression
ad6antr (((((((𝜑𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) → 𝜓)

Proof of Theorem ad6antr
StepHypRef Expression
1 ad2ant.1 . . 3 (𝜑𝜓)
21ad5antr 765 . 2 ((((((𝜑𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)
32adantr 479 1 (((((((𝜑𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  ad7antr  769  catass  16116  funcpropd  16329  natpropd  16405  restutop  21793  utopreg  21808  restmetu  22126  lgamucov  24481  istrkgcb  25072  tgifscgr  25121  tgbtwnconn1lem3  25187  legtrd  25202  miriso  25283  footex  25331  opphllem3  25359  opphl  25364  trgcopy  25414  cgratr  25433  dfcgra2  25439  inaghl  25449  cgrg3col4  25452  f1otrge  25470  cusgrares  25767  clwlkisclwwlklem1  26081  matunitlindflem1  32378  heicant  32417  mblfinlem3  32421  limclner  38522  hoidmvle  39294  clwlkclwwlklem2  41211
  Copyright terms: Public domain W3C validator