Metamath Proof Explorer

Theorem rb-imdf

Description: The definition of implication, in terms of \/ and -. . (Contributed by Anthony Hart, 17-Aug-2011) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	rb-imdf	\|- -. ( -. ( -. ( ph -> ps ) \/ ( -. ph \/ ps ) ) \/ -. ( -. ( -. ph \/ ps ) \/ ( ph -> ps ) ) )

Proof

Step	Hyp	Ref	Expression
1		imor	\|- ( ( ph -> ps ) <-> ( -. ph \/ ps ) )
2		rb-bijust	\|- ( ( ( ph -> ps ) <-> ( -. ph \/ ps ) ) <-> -. ( -. ( -. ( ph -> ps ) \/ ( -. ph \/ ps ) ) \/ -. ( -. ( -. ph \/ ps ) \/ ( ph -> ps ) ) ) )
3	1 2	mpbi	\|- -. ( -. ( -. ( ph -> ps ) \/ ( -. ph \/ ps ) ) \/ -. ( -. ( -. ph \/ ps ) \/ ( ph -> ps ) ) )

Step

Hyp

Ref

Expression

imor

 |-  ( ( ph -> ps ) <-> ( -. ph \/ ps ) )

rb-bijust

 |-  ( ( ( ph -> ps ) <-> ( -. ph \/ ps ) ) <-> -. ( -. ( -. ( ph -> ps ) \/ ( -. ph \/ ps ) ) \/ -. ( -. ( -. ph \/ ps ) \/ ( ph -> ps ) ) ) )

1 2

mpbi

 |-  -. ( -. ( -. ( ph -> ps ) \/ ( -. ph \/ ps ) ) \/ -. ( -. ( -. ph \/ ps ) \/ ( ph -> ps ) ) )