ILE Home 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