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  2093  nfeuv  2098  bm1.1  2217  abbibcom  2346  abbib  2350  nfeq  2392  cleqf  2409  sbhypf  2864  ceqsexg  2945  elabgt  2958  elabgf  2959  copsex2t  4361  copsex2g  4362  opelopabsb  4378  opeliunxp2  4895  ralxpf  4901  rexxpf  4902  cbviota  5317  sb8iota  5320  fmptco  5843  nfiso  5979  uchoice  6331  dfoprab4f  6387  opeliunxp2f  6469  xpf1o  7097  bdsepnfALT  16659