Theorem exnal 1036

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 1032	. 2 |- (A.xph <-> -. E.x -. ph)
2	1	con2bii 221	1 |- (E.x -. ph <-> -. A.xph)

Syntax hints:  -. wn 2   <-> wb 146  A.wal 952  E.wex 978

This theorem is referenced by:  alexn 1042  19.29 1069  equsex 1150  a12studyALT 1377  cla42gv 1861  cla43gv 1863  nss 2109  notzfaus 2736  dtruALT 2743  nssss 2759  dtru 2767  dvdemo1 2770  intirr 3433  zfcndpow 4948

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

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

Copyright terms: Public domain