Theorem nfbi 1582

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

Syntax hints:   <-> wb 104   T. wtru 1349   F/wnf 1453

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-4 1503  ax-ial 1527  ax-i5r 1528

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454

This theorem is referenced by:  sb8eu  2032  nfeuv  2037  bm1.1  2155  abbi  2284  nfeq  2320  cleqf  2337  sbhypf  2779  ceqsexg  2858  elabgt  2871  elabgf  2872  copsex2t  4230  copsex2g  4231  opelopabsb  4245  opeliunxp2  4751  ralxpf  4757  rexxpf  4758  cbviota  5165  sb8iota  5167  fmptco  5662  nfiso  5785  dfoprab4f  6172  opeliunxp2f  6217  xpf1o  6822  bdsepnfALT  13924