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

Theorem ad6antr 735
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 484 . 2 ((𝜑𝜒) → 𝜓)
32ad5antr 733 1 (((((((𝜑𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  ad7antr  737  ad7antlr  738  simp-6l  786  catass  16949  funcpropd  17162  natpropd  17238  restutop  22843  utopreg  22858  restmetu  23177  lgamucov  25623  istrkgcb  26250  tgifscgr  26302  tgbtwnconn1lem3  26368  legtrd  26383  miriso  26464  footexALT  26512  footex  26515  opphllem3  26543  opphl  26548  trgcopy  26598  cgratr  26617  dfcgra2  26624  inaghl  26639  cgrg3col4  26647  f1otrge  26666  clwlkclwwlklem2  27785  cyc3genpm  30844  elrspunidl  31014  rhmimaidl  31017  ssmxidllem  31049  lbsdiflsp0  31110  dimkerim  31111  fedgmul  31115  txomap  31187  matunitlindflem1  35053  heicant  35092  mblfinlem3  35096  limclner  42291  hoidmvle  43237
  Copyright terms: Public domain W3C validator