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

Theorem ad6antr 736
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 480 . 2 ((𝜑𝜒) → 𝜓)
32ad5antr 734 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:  ad7antr  738  ad7antlr  739  simp-6l  786  catass  17730  funcpropd  17948  natpropd  18025  ghmqusnsg  19301  ghmquskerlem3  19305  rhmqusnsg  21296  restutop  24247  utopreg  24262  restmetu  24584  lgamucov  27082  istrkgcb  28465  tgifscgr  28517  tgbtwnconn1lem3  28583  legtrd  28598  miriso  28679  footexALT  28727  footex  28730  opphllem3  28758  opphl  28763  trgcopy  28813  cgratr  28832  dfcgra2  28839  inaghl  28854  cgrg3col4  28862  f1otrge  28881  clwlkclwwlklem2  30020  gsumwun  33069  cyc3genpm  33173  elrgspnlem4  33250  erler  33270  rlocaddval  33273  rlocmulval  33274  rloccring  33275  rhmquskerlem  33454  elrspunidl  33457  rhmimaidl  33461  ssdifidllem  33485  ssdifidlprm  33487  mxidlirredi  33500  mxidlirred  33501  ssmxidllem  33502  qsdrngi  33524  1arithidom  33566  1arithufdlem3  33575  r1plmhm  33631  r1pquslmic  33632  lbsdiflsp0  33678  dimkerim  33679  fedgmul  33683  fldextrspunlsplem  33724  fldext2chn  33770  constrextdg2lem  33790  txomap  33834  matunitlindflem1  37624  heicant  37663  mblfinlem3  37667  primrootscoprmpow  42101  aks6d1c2lem4  42129  aks6d1c5  42141  limclner  45671  hoidmvle  46620
  Copyright terms: Public domain W3C validator