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

Theorem 19.42vv 1785
 Description: Theorem 19.42 of [Margaris] p. 90 with 2 quantifiers. (Contributed by NM, 16-Mar-1995.)
Assertion
Ref Expression
19.42vv (xy(φ ψ) ↔ (φ xyψ))
Distinct variable groups:   φ,x   φ,y
Allowed substitution hints:   ψ(x,y)

Proof of Theorem 19.42vv
StepHypRef Expression
1 exdistr 1784 . 2 (xy(φ ψ) ↔ x(φ yψ))
2 19.42v 1783 . 2 (x(φ yψ) ↔ (φ xyψ))
31, 2bitri 173 1 (xy(φ ψ) ↔ (φ xyψ))
 Colors of variables: wff set class Syntax hints:   ∧ wa 97   ↔ wb 98  ∃wex 1378 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 This theorem is referenced by:  19.42vvv  1786  19.42vvvv  1787  exdistr2  1788  3exdistr  1789  ceqsex3v  2590  ceqsex4v  2591  elvvv  4346  dfoprab2  5494  resoprab  5539  ovi3  5579  ov6g  5580  oprabex3  5698  xpassen  6240  enq0enq  6414  enq0sym  6415  nqnq0pi  6421
 Copyright terms: Public domain W3C validator