ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  alimdv GIF version

Theorem alimdv 1835
Description: Deduction from Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 3-Apr-1994.)
Hypothesis
Ref Expression
alimdv.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
alimdv (𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)

Proof of Theorem alimdv
StepHypRef Expression
1 ax-17 1491 . 2 (𝜑 → ∀𝑥𝜑)
2 alimdv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2alimdh 1428 1 (𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1314
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1408  ax-gen 1410  ax-17 1491
This theorem is referenced by:  2alimdv  1837  moim  2041  ralimdv2  2479  sstr2  3074  reuss2  3326  ssuni  3728  disjss2  3879  disjss1  3882  disjiun  3894  exmidsssnc  4096  soss  4206  alxfr  4352  ssrel  4597  ssrel2  4599  ssrelrel  4609  iotaval  5069  omnimkv  6998
  Copyright terms: Public domain W3C validator