Theorem 19.26 1680

Description: Theorem 19.26 of [Margaris] p. 90. Also Theorem *10.22 of [WhiteheadRussell] p. 147. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 4-Jul-2014.)

Assertion

Ref	Expression
19.26

Proof of Theorem 19.26

Step	Hyp	Ref	Expression
1		simpl 457	. . . 4
2	1	alimi 1633	. . 3
3		simpr 461	. . . 4
4	3	alimi 1633	. . 3
5	2, 4	jca 532	. 2
6		id 22	. . 3
7	6	alanimi 1637	. 2
8	5, 7	impbii 188	1

Syntax hints:  <->wb 184  /\wa 369  A.wal 1393

This theorem is referenced by:  19.26-2  1681  19.26-3an  1682  19.35OLD  1688  19.43OLD  1694  albiim  1699  2albiim  1700  19.27v  1766  19.28v  1767  19.27  1923  19.28  1924  ax12eq  2271  ax12el  2272  2eu4OLD  2381  bm1.1OLD  2441  r19.26m  2987  unss  3677  ralunb  3684  ssin  3719  intun  4319  intpr  4320  eqrelrel  5109  relop  5158  eqoprab2b  6355  dfer2  7331  axgroth4  9231  grothprim  9233  caubnd  13191  wl-alanbii  30018  dford4  30971  alimp-no-surprise  33196  bj-gl4lem  34183  bj-gl4  34184

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-an 371