Theorem nfbi 1612

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 1611	. 2 |- ( T. -> F/ x ( ph <-> ps ) )
6	5	mptru 1382	1 |- F/ x ( ph <-> ps )

Syntax hints:   <-> wb 105   T. wtru 1374   F/wnf 1483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1470  ax-gen 1472  ax-4 1533  ax-ial 1557  ax-i5r 1558

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484

This theorem is referenced by:  sb8eu  2067  nfeuv  2072  bm1.1  2190  abbi  2319  nfeq  2356  cleqf  2373  sbhypf  2822  ceqsexg  2901  elabgt  2914  elabgf  2915  copsex2t  4290  copsex2g  4291  opelopabsb  4307  opeliunxp2  4819  ralxpf  4825  rexxpf  4826  cbviota  5238  sb8iota  5240  fmptco  5748  nfiso  5877  uchoice  6225  dfoprab4f  6281  opeliunxp2f  6326  xpf1o  6943  bdsepnfALT  15862