Theorem i2i1 267

Description: Correspondence between Sasaki and Dishkant conditionals.

Assertion

Ref	Expression
i2i1	(a ->2 b) = (b' ->1 a')

Proof of Theorem i2i1

Step	Hyp	Ref	Expression
1		ax-a1 30	. . 3 a = a''
2	1	ud2lem0b 259	. 2 (a ->2 b'') = (a'' ->2 b'')
3		ax-a1 30	. . 3 b = b''
4	3	ud2lem0a 258	. 2 (a ->2 b) = (a ->2 b'')
5		i1i2 266	. 2 (b' ->1 a') = (a'' ->2 b'')
6	2, 4, 5	3tr1 63	1 (a ->2 b) = (b' ->1 a')

Syntax hints:   = wb 1  'wn 4   ->1 wi1 12   ->2 wi2 13

This theorem is referenced by:  nom40 325  nom41 326  nom42 327  nom43 328  nom44 329  nom45 330  nom50 331  nom51 332  nom52 333  nom53 334  nom54 335  nom55 336  oal2 999

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

This theorem depends on definitions:  df-a 40  df-i1 44  df-i2 45

Copyright terms: Public domain