MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfbi Structured version   Unicode version

Theorem nfbi 1867
Description: If  x is not free in  ph and  ps, it is not free in  ( ph  <->  ps ). (Contributed by NM, 26-May-1993.) (Revised by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.)
Hypotheses
Ref Expression
nf.1  |-  F/ x ph
nf.2  |-  F/ x ps
Assertion
Ref Expression
nfbi  |-  F/ x
( ph  <->  ps )

Proof of Theorem nfbi
StepHypRef Expression
1 nf.1 . . . 4  |-  F/ x ph
21a1i 11 . . 3  |-  ( T. 
->  F/ x ph )
3 nf.2 . . . 4  |-  F/ x ps
43a1i 11 . . 3  |-  ( T. 
->  F/ x ps )
52, 4nfbid 1866 . 2  |-  ( T. 
->  F/ x ( ph  <->  ps ) )
65trud 1378 1  |-  F/ x
( ph  <->  ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184   T. wtru 1370   F/wnf 1589
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-12 1792
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590
This theorem is referenced by:  euf  2263  eufOLD  2264  sb8eu  2292  sb8euOLD  2293  sb8euOLDOLD  2294  bm1.1  2427  bm1.1OLD  2428  cleqh  2542  abbiOLD  2559  nfeqOLD  2600  cleqfOLD  2616  sbhypf  3040  ceqsexg  3112  elabgt  3124  elabgf  3125  axrep1  4425  axrep3  4427  axrep4  4428  copsex2t  4599  copsex2g  4600  opelopabsb  4620  opeliunxp2  4999  ralxpf  5007  cbviota  5407  sb8iota  5409  fvopab5  5816  fmptco  5897  nfiso  6036  dfoprab4f  6653  xpf1o  7494  zfcndrep  8802  uzindOLD  10757  gsumcom2  16489  isfildlem  19452  cnextfvval  19659  mbfsup  21164  mbfinf  21165  fmptcof2  26001  subtr2  28536  sbcalf  28946  sbcexf  28947  mpt2bi123f  29001  bnj1468  31935  bj-abbi  32392  bj-axrep1  32405  bj-axrep3  32407  bj-axrep4  32408
  Copyright terms: Public domain W3C validator