Theorem nfbi 1642

Description: If x is not free in ph and ps, then it is not free in ( ph <-> ps ). (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.)

Hypotheses

Ref	Expression
nfbi.1	|- F/ x ph
nfbi.2	|- F/ x ps

Assertion

Ref	Expression
nfbi	|- F/ x ( ph <-> ps )

Proof of Theorem nfbi

Step	Hyp	Ref	Expression
1		nfbi.1	. . . 4 |- F/ x ph
2	1	a1i 9	. . 3 |- ( T. -> F/ x ph )
3		nfbi.2	. . . 4 |- F/ x ps
4	3	a1i 9	. . 3 |- ( T. -> F/ x ps )
5	2, 4	nfbid 1641	. 2 |- ( T. -> F/ x ( ph <-> ps ) )
6	5	mptru 1411	1 |- F/ x ( ph <-> ps )

This proof depends on syntax axioms:   <-> wb 105   T. wtru 1403   F/wnf 1513

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-ial 1587  ax-i5r 1588

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514

This theorem is used by:  sb8eu  2099  nfeuv  2104  bm1.1  2223  abbibcom  2352  abbib  2356  nfeq  2400  cleqf  2417  sbhypf  2872  ceqsexg  2954  elabgt  2967  elabgf  2968  copsex2t  4387  copsex2g  4388  opelopabsb  4404  opeliunxp2  4922  ralxpf  4928  rexxpf  4929  cbviota  5345  sb8iota  5348  fmptco  5877  nfiso  6015  uchoice  6375  dfoprab4f  6431  opeliunxp2f  6513  xpf1o  7148  gsumcom2fi  14275  bdsepnfALT  17120