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

Theorem ralimdv2 2500
 Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 1-Feb-2005.)
Hypothesis
Ref Expression
ralimdv2.1 (𝜑 → ((𝑥𝐴𝜓) → (𝑥𝐵𝜒)))
Assertion
Ref Expression
ralimdv2 (𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐵 𝜒))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)   𝐵(𝑥)

Proof of Theorem ralimdv2
StepHypRef Expression
1 ralimdv2.1 . . 3 (𝜑 → ((𝑥𝐴𝜓) → (𝑥𝐵𝜒)))
21alimdv 1851 . 2 (𝜑 → (∀𝑥(𝑥𝐴𝜓) → ∀𝑥(𝑥𝐵𝜒)))
3 df-ral 2419 . 2 (∀𝑥𝐴 𝜓 ↔ ∀𝑥(𝑥𝐴𝜓))
4 df-ral 2419 . 2 (∀𝑥𝐵 𝜒 ↔ ∀𝑥(𝑥𝐵𝜒))
52, 3, 43imtr4g 204 1 (𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐵 𝜒))
 Colors of variables: wff set class Syntax hints:   → wi 4  ∀wal 1329   ∈ wcel 1480  ∀wral 2414 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-17 1506 This theorem depends on definitions:  df-bi 116  df-ral 2419 This theorem is referenced by:  ssralv  3156  r19.29uz  10757  iscnp4  12376  cnntr  12383
 Copyright terms: Public domain W3C validator