Metamath Proof Explorer


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 ) ) )