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

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

Proof of Theorem 19.41v
StepHypRef Expression
1 ax-17 1416 . 2 (ψxψ)
2119.41h 1572 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:  19.41vv  1780  19.41vvv  1781  19.41vvvv  1782  eeeanv  1805  gencbvex  2594  euxfrdc  2721  euind  2722  r19.9rmv  3307  opabm  4008  eliunxp  4418  relop  4429  dmuni  4488  dmres  4575  dminss  4681  imainss  4682  ssrnres  4706  cnvresima  4753  resco  4768  rnco  4770  coass  4782  xpcom  4807  f11o  5102  fvelrnb  5164  rnoprab  5529  domen  6168  xpassen  6240  genpassl  6507  genpassu  6508
 Copyright terms: Public domain W3C validator