Theorem nfbi 1638

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

Syntax hints:   <-> wb 105   T. wtru 1399   F/wnf 1509

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 1496  ax-gen 1498  ax-4 1559  ax-ial 1583  ax-i5r 1584

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510

This theorem is referenced by:  sb8eu  2095  nfeuv  2100  bm1.1  2219  abbibcom  2348  abbib  2352  nfeq  2394  cleqf  2411  sbhypf  2866  ceqsexg  2948  elabgt  2961  elabgf  2962  copsex2t  4366  copsex2g  4367  opelopabsb  4383  opeliunxp2  4900  ralxpf  4906  rexxpf  4907  cbviota  5322  sb8iota  5325  fmptco  5848  nfiso  5985  uchoice  6344  dfoprab4f  6400  opeliunxp2f  6482  xpf1o  7110  bdsepnfALT  16785