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

Theorem alimdv 1807
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 1464 . 2 (𝜑 → ∀𝑥𝜑)
2 alimdv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2alimdh 1401 1 (𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1287
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-5 1381  ax-gen 1383  ax-17 1464
This theorem is referenced by:  2alimdv  1809  moim  2012  ralimdv2  2443  sstr2  3030  reuss2  3277  ssuni  3670  disjss2  3817  disjss1  3820  disjiun  3832  soss  4132  alxfr  4274  ssrel  4514  ssrel2  4516  ssrelrel  4526  iotaval  4978
  Copyright terms: Public domain W3C validator