Theorem nfbi 1549

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

Syntax hints:   <-> wb 104   T. wtru 1313   F/wnf 1417

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-gen 1406  ax-4 1468  ax-ial 1495  ax-i5r 1496

This theorem depends on definitions:  df-bi 116  df-tru 1315  df-nf 1418

This theorem is referenced by:  sb8eu  1986  nfeuv  1991  bm1.1  2098  abbi  2226  nfeq  2261  cleqf  2277  sbhypf  2704  ceqsexg  2781  elabgt  2793  elabgf  2794  copsex2t  4125  copsex2g  4126  opelopabsb  4140  opeliunxp2  4637  ralxpf  4643  rexxpf  4644  cbviota  5049  sb8iota  5051  fmptco  5538  nfiso  5659  dfoprab4f  6042  opeliunxp2f  6086  xpf1o  6688  bdsepnfALT  12766  strcollnfALT  12863