Theorem con3 65

Description: Contraposition inference.

Hypothesis

Ref	Expression
con3.1	a_|_ = b

Assertion

Ref	Expression
con3	a = b_|_

Proof of Theorem con3

Step	Hyp	Ref	Expression
1		ax-a1 29	. 2 a = a_|__|_
2		con3.1	. . 3 a_|_ = b
3	2	ax-r4 36	. 2 a_|__|_ = b_|_
4	1, 3	ax-r2 35	1 a = b_|_

Syntax hints:   = wb 1  _|_wn 4

This theorem is referenced by:  anor3 82  oran1 83  oran2 84  oran3 85  lecon 146  wlem3.1 202  wwcomd 206  wwfh1 208  ud1lem0c 269  nom12 301  nom13 302  lem3.1 425  comd 438  fh1 451  i3bi 478  ud1lem3 544  ud2lem2 546  ud3lem1a 548  ud3lem2 553  ud4lem1a 559  ud4lem2 564  ud5lem1b 569  ud5lem1 571  ud5lem3 576  u4lemona 610  u2lemnonb 658  oa6to4h1 935  oa6to4h2 936  oa6to4h3 937

This theorem was proved from axioms:  ax-a1 29  ax-r2 35  ax-r4 36

metamath.org