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

Theorem nfbi 1994
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 1993 . 2  |-  ( T. 
->  F/ x ( ph  <->  ps ) )
65trud 1446 1  |-  F/ x
( ph  <->  ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187   T. wtru 1438   F/wnf 1661
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-12 1909
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662
This theorem is referenced by:  euf  2277  sb8eu  2302  bm1.1  2406  cleqh  2532  abbiOLD  2549  nfeqOLD  2592  cleqfOLD  2608  sbhypf  3128  ceqsexg  3202  elabgt  3214  elabgf  3215  axrep1  4537  axrep3  4539  axrep4  4540  copsex2t  4707  copsex2g  4708  opelopabsb  4730  opeliunxp2  4992  ralxpf  5000  cbviota  5570  sb8iota  5572  fvopab5  5990  fmptco  6072  nfiso  6231  dfoprab4f  6866  opeliunxp2f  6968  xpf1o  7744  zfcndrep  9047  gsumcom2  17607  isfildlem  20871  cnextfvval  21079  mbfsup  22619  mbfinf  22620  mbfinfOLD  22621  brabgaf  28219  fmptcof2  28262  bnj1468  29666  subtr2  30977  bj-abbi  31361  bj-axrep1  31374  bj-axrep3  31376  bj-axrep4  31377  mpt2bi123f  32371  fourierdlem31  37941  fourierdlem31OLD  37942
  Copyright terms: Public domain W3C validator