Metamath Proof Explorer


Theorem nfnbiOLD

Description: Obsolete version of nfnbi as of 6-Oct-2024. (Contributed by BJ, 6-May-2019) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion nfnbiOLD
|- ( F/ x ph <-> F/ x -. ph )

Proof

Step Hyp Ref Expression
1 orcom
 |-  ( ( A. x ph \/ A. x -. ph ) <-> ( A. x -. ph \/ A. x ph ) )
2 nf3
 |-  ( F/ x ph <-> ( A. x ph \/ A. x -. ph ) )
3 nf3
 |-  ( F/ x -. ph <-> ( A. x -. ph \/ A. x -. -. ph ) )
4 notnotb
 |-  ( ph <-> -. -. ph )
5 4 albii
 |-  ( A. x ph <-> A. x -. -. ph )
6 5 orbi2i
 |-  ( ( A. x -. ph \/ A. x ph ) <-> ( A. x -. ph \/ A. x -. -. ph ) )
7 3 6 bitr4i
 |-  ( F/ x -. ph <-> ( A. x -. ph \/ A. x ph ) )
8 1 2 7 3bitr4i
 |-  ( F/ x ph <-> F/ x -. ph )