Theorem i2i1 259

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 29	. . 3 a = a⊥ ⊥
2	1	ud2lem0b 251	. 2 (a →2 b⊥ ⊥ ) = (a⊥ ⊥ →2 b⊥ ⊥ )
3		ax-a1 29	. . 3 b = b⊥ ⊥
4	3	ud2lem0a 250	. 2 (a →2 b) = (a →2 b⊥ ⊥ )
5		i1i2 258	. 2 (b⊥ →1 a⊥ ) = (a⊥ ⊥ →2 b⊥ ⊥ )
6	2, 4, 5	3tr1 60	1 (a →2 b) = (b⊥ →1 a⊥ )

Syntax hints:   = wb 1  ^⊥ wn 4   →₁ wi1 13   →₂ wi2 14

This theorem is referenced by:  nom40 317  nom41 318  nom42 319  nom43 320  nom44 321  nom45 322  nom50 323  nom51 324  nom52 325  nom53 326  nom54 327  nom55 328  oal2 979

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

This theorem depends on definitions:  df-a 39  df-i1 43  df-i2 44

metamath.org