Theorem nfbi 1587

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

Syntax hints:   <-> wb 105   T. wtru 1354   F/wnf 1458

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 1445  ax-gen 1447  ax-4 1508  ax-ial 1532  ax-i5r 1533

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1459

This theorem is referenced by:  sb8eu  2037  nfeuv  2042  bm1.1  2160  abbi  2289  nfeq  2325  cleqf  2342  sbhypf  2784  ceqsexg  2863  elabgt  2876  elabgf  2877  copsex2t  4239  copsex2g  4240  opelopabsb  4254  opeliunxp2  4760  ralxpf  4766  rexxpf  4767  cbviota  5175  sb8iota  5177  fmptco  5674  nfiso  5797  dfoprab4f  6184  opeliunxp2f  6229  xpf1o  6834  bdsepnfALT  14181