Theorem pm2.04 82

Description: Swap antecedents. Theorem *2.04 of [WhiteheadRussell] p. 100. This was the third axiom in Frege's logic system, specifically Proposition 8 of [Frege1879] p. 35. Its associated inference is com12 31. (Contributed by NM, 27-Dec-1992.) (Proof shortened by Wolf Lammen, 12-Sep-2012.)

Assertion

Ref	Expression
pm2.04

Proof of Theorem pm2.04

Step	Hyp	Ref	Expression
1		id 22	. 2
2	1	com23 78	1

Syntax hints:  ->wi 4

This theorem is referenced by:  com34  83  com45  89  bi2.04  361  merco2  1569  ralcom3  3023  rexrsb  32174  syl5imp  33282  com3rgbi  33284  syl5impVD  33663  simplbi2comtVD  33688  19.41rgVD  33702  ax6e2eqVD  33707

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