Theorem exbi 1666

Description: Theorem 19.18 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)

Assertion

Ref	Expression
exbi

Proof of Theorem exbi

Step	Hyp	Ref	Expression
1		bi1 186	. . 3
2	1	aleximi 1653	. 2
3		bi2 198	. . 3
4	3	aleximi 1653	. 2
5	2, 4	impbid 191	1

Syntax hints:  ->wi 4  <->wb 184  A.wal 1393  E.wex 1612

This theorem is referenced by:  exbii  1667  exbidh  1676  exintrbi  1701  19.19  1959  2exbi  31285  rexbidar  31355  onfrALTlem5VD  33685  onfrALTlem1VD  33690  csbxpgVD  33694  csbrngVD  33696  csbunigVD  33698  e2ebindVD  33712  e2ebindALT  33729  bnj956  33835  bj-2exbi  34206  bj-3exbi  34207  bj-nfbi  34217

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631

This theorem depends on definitions:  df-bi 185  df-ex 1613