Theorem con2 67

Description: Contraposition inference.

Hypothesis

Ref	Expression
con2.1	a = b'

Assertion

Ref	Expression
con2	a' = b

Proof of Theorem con2

Step	Hyp	Ref	Expression
1		con2.1	. . 3 a = b'
2	1	ax-r4 37	. 2 a' = b''
3		ax-a1 30	. . 3 b = b''
4	3	ax-r1 35	. 2 b'' = b
5	2, 4	ax-r2 36	1 a' = b

Syntax hints:   = wb 1  'wn 4

This theorem is referenced by:  anass 76  dfb 94  dfnb 95  an1 106  an0 108  anidm 111  a5c 121  mi 125  comm0 178  wwfh1 216  wwfh2 217  wwfh3 218  wwfh4 219  ka4lemo 228  ka4lem 229  ska10 238  lei3 246  ni31 250  0i1 273  ud1lem0c 277  ud2lem0c 278  ud4lem0c 280  ud5lem0c 281  wcom2an 428  omla 447  comcom 453  comd 456  comdr 466  com3i 467  df2c1 468  fh1 469  fh2 470  com2an 484  i3bi 496  ni32 502  lem4 511  i3th1 543  i3con 551  i3orlem5 556  ud1lem2 561  ud2lem2 564  ud4lem1a 577  ud4lem1c 579  ud4lem1 581  ud4lem2 582  ud5lem3c 593  u3lemob 632  u3lemonb 637  u5lemnaa 644  u1lemnab 650  u2lemnab 651  u3lemnab 652  u3lem1n 741  u5lem1n 743  u3lem3n 754  u4lem3n 755  u5lem3n 756  u4lem5n 766  u2lem7n 775  u3lem11a 787  gomaex3 924  lem3.3.4 1052

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

Copyright terms: Public domain