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

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

Proof of Theorem ad7antr
StepHypRef Expression
1 ad2ant.1 . . 3 (𝜑𝜓)
21adantr 480 . 2 ((𝜑𝜒) → 𝜓)
32ad6antr 736 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:  ad8antr  740  ad8antlr  741  simp-7l  789  catpropd  17752  natpropd  18024  ucncn  24294  tgcgrxfr  28526  tgbtwnconn1lem3  28582  tgbtwnconn1  28583  midexlem  28700  lnopp2hpgb  28771  trgcopy  28812  mgcf1o  32993  chnub  33002  elrgspnlem4  33249  elrspunidl  33456  rhmimaidl  33460  qsidomlem2  33481  ssdifidlprm  33486  mxidlirredi  33499  1arithufdlem3  33574  lbsdiflsp0  33677  fedgmul  33682  constrconj  33786  constrelextdg2  33788  zarcmplem  33880  sigapildsys  34163  afsval  34686  matunitlindflem1  37623  aks6d1c2lem4  42128  dffltz  42644
  Copyright terms: Public domain W3C validator