Theorem rb-bijust

Description: Justification for rb-imdf . (Contributed by Anthony Hart, 17-Aug-2011) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		dfbi1	|- ( ( ph <-> ps ) <-> -. ( ( ph -> ps ) -> -. ( ps -> ph ) ) )
2		imor	|- ( ( ph -> ps ) <-> ( -. ph \/ ps ) )
3		imor	|- ( ( ps -> ph ) <-> ( -. ps \/ ph ) )
4	3	notbii	|- ( -. ( ps -> ph ) <-> -. ( -. ps \/ ph ) )
5	2 4	imbi12i	|- ( ( ( ph -> ps ) -> -. ( ps -> ph ) ) <-> ( ( -. ph \/ ps ) -> -. ( -. ps \/ ph ) ) )
6	5	notbii	|- ( -. ( ( ph -> ps ) -> -. ( ps -> ph ) ) <-> -. ( ( -. ph \/ ps ) -> -. ( -. ps \/ ph ) ) )
7		pm4.62	|- ( ( ( -. ph \/ ps ) -> -. ( -. ps \/ ph ) ) <-> ( -. ( -. ph \/ ps ) \/ -. ( -. ps \/ ph ) ) )
8	7	notbii	|- ( -. ( ( -. ph \/ ps ) -> -. ( -. ps \/ ph ) ) <-> -. ( -. ( -. ph \/ ps ) \/ -. ( -. ps \/ ph ) ) )
9	1 6 8	3bitri	|- ( ( ph <-> ps ) <-> -. ( -. ( -. ph \/ ps ) \/ -. ( -. ps \/ ph ) ) )