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

Theorem r19.41v 2460
 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 1418 . 2 xψ
21r19.41 2459 1 (x A (φ ψ) ↔ (x A φ ψ))
 Colors of variables: wff set class Syntax hints:   ∧ wa 97   ↔ wb 98  ∃wrex 2301 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 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-17 1416  ax-ial 1424 This theorem depends on definitions:  df-bi 110  df-nf 1347  df-rex 2306 This theorem is referenced by:  r19.42v  2461  3reeanv  2474  reuind  2738  iuncom4  3655  dfiun2g  3680  iunxiun  3727  inuni  3900  xpiundi  4341  xpiundir  4342  imaco  4769  coiun  4773  abrexco  5341  imaiun  5342  isoini  5400  rexrnmpt2  5558  genpassl  6507  genpassu  6508  4fvwrd4  8767
 Copyright terms: Public domain W3C validator