Theorem 19.26 1648

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 1605	. . 3
3		simpr 461	. . . 4
4	3	alimi 1605	. . 3
5	2, 4	jca 532	. 2
6		id 22	. . 3
7	6	alanimi 1608	. 2
8	5, 7	impbii 188	1

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

This theorem is referenced by:  19.26-2  1649  19.26-3an  1650  19.35OLD  1656  19.43OLD  1662  albiim  1666  2albiim  1667  19.27  1857  19.28  1858  ax12eq  2248  ax12el  2249  2eu4OLD  2375  bm1.1OLD  2434  r19.26m  2932  unss  3612  ralunb  3619  ssin  3654  intun  4242  intpr  4243  eqrelrel  5023  relop  5072  eqoprab2b  6227  dfer2  7186  axgroth4  9084  grothprim  9086  caubnd  12932  wl-alanbii  28516  dford4  29500  alimp-no-surprise  31414

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

This theorem depends on definitions:  df-bi 185  df-an 371