New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  19.42vv GIF version

Theorem 19.42vv 1907
 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 1906 . 2 (xy(φ ψ) ↔ x(φ yψ))
2 19.42v 1905 . 2 (x(φ yψ) ↔ (φ xyψ))
31, 2bitri 240 1 (xy(φ ψ) ↔ (φ xyψ))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 176   ∧ wa 358  ∃wex 1541 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-11 1746 This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-nf 1545 This theorem is referenced by:  19.42vvv  1908  exdistr2  1909  3exdistr  1910  ceqsex3v  2897  ceqsex4v  2898  ceqsex8v  2900  otkelins2kg  4253  otkelins3kg  4254  opkelcokg  4261  sikexlem  4295  insklem  4304  elswap  4740  dmsi  5519  dfoprab2  5558  resoprab  5581  ov3  5599  ov6g  5600  brpprod  5839  dmpprod  5840  lecex  6115  ce0nnul  6177
 Copyright terms: Public domain W3C validator