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

Theorem ralimdv 2405
 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 265 . 2 ((𝜑𝑥𝐴) → (𝜓𝜒))
32ralimdva 2404 1 (𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 𝜒))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∈ wcel 1409  ∀wral 2323 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-4 1416  ax-17 1435 This theorem depends on definitions:  df-bi 114  df-nf 1366  df-ral 2328 This theorem is referenced by:  poss  4063  sess1  4102  sess2  4103  riinint  4621  dffo4  5343  dffo5  5344  isoini2  5486  rdgivallem  5999  iinerm  6209  resqrexlemgt0  9847  cau3lem  9941  caubnd2  9944  climshftlemg  10054  climcau  10097  climcaucn  10101  serif0  10102
 Copyright terms: Public domain W3C validator