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

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

Proof of Theorem ralimdva
StepHypRef Expression
1 nfv 1437 . 2 𝑥𝜑
2 ralimdva.1 . 2 ((𝜑𝑥𝐴) → (𝜓𝜒))
31, 2ralimdaa 2403 1 (𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 𝜒))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 101   ∈ 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:  ralimdv  2405  f1mpt  5438  isores3  5483  caofrss  5763  caoftrn  5764  tfrlemibxssdm  5972  rdgon  6004  caucvgsrlemoffcau  6940  caucvgsrlemoffres  6942  indstr  8632  caucvgre  9808  rexuz3  9817  resqrexlemgt0  9847  resqrexlemglsq  9849  cau3lem  9941  2clim  10053  climcn1  10060  climcn2  10061  subcn2  10063  climsqz  10086  climsqz2  10087  climcvg1nlem  10099
 Copyright terms: Public domain W3C validator