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

Theorem 19.42v 1783
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 1416 . 2 (φxφ)
2119.42h 1574 1 (x(φ ψ) ↔ (φ xψ))
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:  exdistr  1784  19.42vv  1785  19.42vvv  1786  4exdistr  1790  cbvex2  1794  2sb5  1856  2sb5rf  1862  rexcom4a  2572  ceqsex2  2588  reuind  2738  2rmorex  2739  sbccomlem  2826  bm1.3ii  3869  opm  3962  eqvinop  3971  uniuni  4149  dmopabss  4490  dmopab3  4491  mptpreima  4757  brprcneu  5114  relelfvdm  5148  fndmin  5217  fliftf  5382  dfoprab2  5494  dmoprab  5527  dmoprabss  5528  fnoprabg  5544  opabex3d  5690  opabex3  5691  eroveu  6133  dmaddpq  6363  dmmulpq  6364  prarloc  6486  ltexprlemopl  6575  ltexprlemlol  6576  ltexprlemopu  6577  ltexprlemupu  6578  bdbm1.3ii  9346
  Copyright terms: Public domain W3C validator