Theorem exnal 1038

Description: Theorem 19.14 of [Margaris] p. 90.

Assertion

Ref	Expression
exnal	|- (E.x -. ph <-> -. A.xph)

Proof of Theorem exnal

Step	Hyp	Ref	Expression
1		alex 1034	. 2 |- (A.xph <-> -. E.x -. ph)
2	1	con2bii 221	1 |- (E.x -. ph <-> -. A.xph)

Syntax hints:  -. wn 2   <-> wb 146  A.wal 954  E.wex 980

This theorem is referenced by:  alexn 1044  19.29 1071  equsex 1152  a12studyALT 1379  cla42gv 1865  cla43gv 1867  nss 2113  notzfaus 2741  dtruALT 2748  nssss 2764  dtru 2772  dvdemo1 2775  intirr 3441  zfcndpow 4968

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-4 973  ax-5o 975

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981

Copyright terms: Public domain