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

Theorem ralimdv 2500
 Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 8-Oct-2003.)
Hypothesis
Ref Expression
ralimdv.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
ralimdv (𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 𝜒))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem ralimdv
StepHypRef Expression
1 ralimdv.1 . . 3 (𝜑 → (𝜓𝜒))
21adantr 274 . 2 ((𝜑𝑥𝐴) → (𝜓𝜒))
32ralimdva 2499 1 (𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 𝜒))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∈ wcel 1480  ∀wral 2416 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-4 1487  ax-17 1506 This theorem depends on definitions:  df-bi 116  df-nf 1437  df-ral 2421 This theorem is referenced by:  poss  4220  sess1  4259  sess2  4260  riinint  4800  dffo4  5568  dffo5  5569  isoini2  5720  rdgivallem  6278  iinerm  6501  xpf1o  6738  resqrexlemgt0  10792  cau3lem  10886  caubnd2  10889  climshftlemg  11071  climcau  11116  climcaucn  11120  serf0  11121  modfsummodlemstep  11226  bezoutlemmain  11686  ctinf  11943  strsetsid  11992  fiinbas  12216  baspartn  12217  lmtopcnp  12419  rescncf  12737  limcresi  12804
 Copyright terms: Public domain W3C validator