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

Theorem 19.42v 1768
Description: Special case of Theorem 19.42 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
19.42v (x(φ ψ) ↔ (φ xψ))
Distinct variable group:   φ,x
Allowed substitution hint:   ψ(x)

Proof of Theorem 19.42v
StepHypRef Expression
1 ax-17 1400 . 2 (φxφ)
2119.42h 1559 1 (x(φ ψ) ↔ (φ xψ))
Colors of variables: wff set class
Syntax hints:   wa 97  wb 98  wex 1362
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 1316  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-4 1381  ax-17 1400  ax-ial 1409
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  exdistr  1769  19.42vv  1770  19.42vvv  1771  4exdistr  1775  cbvex2  1779  2sb5  1841  2sb5rf  1847  rexcom4a  2555  ceqsex2  2571  reuind  2721  2rmorex  2722  sbccomlem  2809  bm1.3ii  3852  opm  3945  eqvinop  3954  uniuni  4133  dmopabss  4474  dmopab3  4475  mptpreima  4741  brprcneu  5096  relelfvdm  5130  fndmin  5199  fliftf  5364  dfoprab2  5475  dmoprab  5508  dmoprabss  5509  fnoprabg  5525  opabex3d  5671  opabex3  5672  eroveu  6108  dmaddpq  6238  dmmulpq  6239  prarloc  6357  ltexprlemopl  6438  ltexprlemlol  6439  ltexprlemopu  6440  ltexprlemupu  6441  bdbm1.3ii  7117
  Copyright terms: Public domain W3C validator