ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  r19.41v Structured version   GIF version

Theorem r19.41v 2435
Description: Restricted quantifier version of Theorem 19.41 of [Margaris] p. 90. (Contributed by NM, 17-Dec-2003.)
Assertion
Ref Expression
r19.41v (x A (φ ψ) ↔ (x A φ ψ))
Distinct variable group:   ψ,x
Allowed substitution hints:   φ(x)   A(x)

Proof of Theorem r19.41v
StepHypRef Expression
1 nfv 1394 . 2 xψ
21r19.41 2434 1 (x A (φ ψ) ↔ (x A φ ψ))
Colors of variables: wff set class
Syntax hints:   wa 97  wb 98  wrex 2276
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 1309  ax-gen 1311  ax-ie1 1355  ax-ie2 1356  ax-4 1373  ax-17 1392  ax-ial 1400
This theorem depends on definitions:  df-bi 110  df-nf 1323  df-rex 2281
This theorem is referenced by:  r19.42v  2436  3reeanv  2449  reuind  2712  iuncom4  3627  dfiun2g  3652  iunxiun  3699  inuni  3872  xpiundi  4313  xpiundir  4314  imaco  4741  coiun  4745  abrexco  5311  imaiun  5312  isoini  5370  rexrnmpt2  5527  genpassl  6365  genpassu  6366
  Copyright terms: Public domain W3C validator