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

Theorem r19.42v 2441
Description: Restricted version of Theorem 19.42 of [Margaris] p. 90. (Contributed by NM, 27-May-1998.)
Assertion
Ref Expression
r19.42v (x A (φ ψ) ↔ (φ x A ψ))
Distinct variable group:   φ,x
Allowed substitution hints:   ψ(x)   A(x)

Proof of Theorem r19.42v
StepHypRef Expression
1 r19.41v 2440 . 2 (x A (ψ φ) ↔ (x A ψ φ))
2 ancom 253 . . 3 ((φ ψ) ↔ (ψ φ))
32rexbii 2305 . 2 (x A (φ ψ) ↔ x A (ψ φ))
4 ancom 253 . 2 ((φ x A ψ) ↔ (x A ψ φ))
51, 3, 43bitr4i 201 1 (x A (φ ψ) ↔ (φ x A ψ))
Colors of variables: wff set class
Syntax hints:   wa 97  wb 98  wrex 2281
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 1312  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-4 1377  ax-17 1396  ax-ial 1405
This theorem depends on definitions:  df-bi 110  df-tru 1229  df-nf 1326  df-rex 2286
This theorem is referenced by:  ceqsrexbv  2648  ceqsrex2v  2649  2reuswapdc  2716  iunrab  3674  iunin2  3690  iundif2ss  3692  iunopab  3988  elxp2  4286  cnvuni  4444  elunirn  5326  f1oiso  5386  oprabrexex2  5676  genpdflem  6355  1idprl  6423  1idpru  6424  ltexprlemm  6431
  Copyright terms: Public domain W3C validator