Theorem con3 68

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 30	. 2 a = a''
2		con3.1	. . 3 a' = b
3	2	ax-r4 37	. 2 a'' = b'
4	1, 3	ax-r2 36	1 a = b'

Syntax hints:   = wb 1  'wn 4

This theorem is referenced by:  anor3 90  oran1 91  oran2 92  oran3 93  lecon 154  wlem3.1 210  wwcomd 214  wwfh1 216  ud1lem0c 277  nom12 309  nom13 310  comd 456  fh1 469  i3bi 496  ud1lem3 562  ud2lem2 564  ud3lem1a 566  ud3lem2 571  ud4lem1a 577  ud4lem2 582  ud5lem1b 587  ud5lem1 589  ud5lem3 594  u4lemona 628  u2lemnonb 676  oa6to4h1 955  oa6to4h2 956  oa6to4h3 957  lem3.3.4 1052

This theorem was proved from axioms:  ax-a1 30  ax-r2 36  ax-r4 37

Copyright terms: Public domain