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

Theorem ad6antr 779
Description: Deduction adding 6 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
ad6antr (((((((𝜑𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) → 𝜓)

Proof of Theorem ad6antr
StepHypRef Expression
1 ad2ant.1 . . 3 (𝜑𝜓)
21adantr 472 . 2 ((𝜑𝜒) → 𝜓)
32ad5antr 775 1 (((((((𝜑𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 197  df-an 385
This theorem is referenced by:  ad7antr  783  ad7antrOLD  784  ad7antlr  785  simp-6l  833  simp-7r  839  catass  16569  funcpropd  16782  natpropd  16858  restutop  22263  utopreg  22278  restmetu  22597  lgamucov  24985  istrkgcb  25576  tgifscgr  25624  tgbtwnconn1lem3  25690  legtrd  25705  miriso  25786  footex  25834  opphllem3  25862  opphl  25867  trgcopy  25917  cgratr  25936  dfcgra2  25942  inaghl  25952  cgrg3col4  25955  f1otrge  25973  clwlkclwwlklem2  27145  matunitlindflem1  33737  heicant  33776  mblfinlem3  33780  limclner  40405  hoidmvle  41339
  Copyright terms: Public domain W3C validator