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

Theorem r19.42v 2461
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 2460 . 2 (x A (ψ φ) ↔ (x A ψ φ))
2 ancom 253 . . 3 ((φ ψ) ↔ (ψ φ))
32rexbii 2325 . 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 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-tru 1245  df-nf 1347  df-rex 2306
This theorem is referenced by:  ceqsrexbv  2669  ceqsrex2v  2670  2reuswapdc  2737  iunrab  3695  iunin2  3711  iundif2ss  3713  iunopab  4009  elxp2  4306  cnvuni  4464  elunirn  5348  f1oiso  5408  oprabrexex2  5699  genpdflem  6489  1idprl  6565  1idpru  6566  ltexprlemm  6573  rexuz2  8280  4fvwrd4  8747
  Copyright terms: Public domain W3C validator