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

Theorem ralbidva 2322
 Description: Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 4-Mar-1997.)
Hypothesis
Ref Expression
ralbidva.1 ((𝜑𝑥𝐴) → (𝜓𝜒))
Assertion
Ref Expression
ralbidva (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐴 𝜒))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem ralbidva
StepHypRef Expression
1 nfv 1421 . 2 𝑥𝜑
2 ralbidva.1 . 2 ((𝜑𝑥𝐴) → (𝜓𝜒))
31, 2ralbida 2320 1 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐴 𝜒))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   ∈ wcel 1393  ∀wral 2306 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-4 1400  ax-17 1419 This theorem depends on definitions:  df-bi 110  df-nf 1350  df-ral 2311 This theorem is referenced by:  raleqbidva  2519  poinxp  4409  funimass4  5224  funimass3  5283  funconstss  5285  cocan1  5427  cocan2  5428  isocnv2  5452  isores2  5453  isoini2  5458  ofrfval  5720  ofrfval2  5727  dfsmo2  5902  smores  5907  smores2  5909  ac6sfi  6352  ordiso2  6357  caucvgsrlemcau  6877  zextlt  8332  prime  8337  fzshftral  8970  clim  9802  clim2  9804  clim2c  9805  clim0c  9807  climabs0  9828  climrecvg1n  9867  sqrt2irr  9878
 Copyright terms: Public domain W3C validator