Theorem pm4.56 495

Description: Theorem *4.56 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)

Assertion

Ref	Expression
pm4.56

Proof of Theorem pm4.56

Step	Hyp	Ref	Expression
1		ioran 490	. 2
2	1	bicomi 202	1

Syntax hints:  -.wn 3  <->wb 184  \/wo 368  /\wa 369

This theorem is referenced by:  oran  496  neanior  2782  prneimg  4211  ordtri3  4919  ssxr  9675  isirred2  17350  aaliou3lem9  22746  coltr2  24028  mideulem2  24108  opphllem  24109  jm2.26lem3  30943  wopprc  30972  icccncfext  31690  cncfiooicc  31697  fourierdlem25  31914  fourierdlem35  31924  fourierswlem  32013  fouriersw  32014  etransclem44  32061  islininds2  33085  iunconlem2  33735  bj-dfbi4  34154  dalawlem13  35607  cdleme22b  36067

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

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