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

Theorem nfbi 2028
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 2027 . 2  |-  ( T. 
->  F/ x ( ph  <->  ps ) )
65trud 1464 1  |-  F/ x
( ph  <->  ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189   T. wtru 1456   F/wnf 1678
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-12 1944
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679
This theorem is referenced by:  euf  2318  sb8eu  2343  bm1.1  2447  cleqh  2563  sbhypf  3107  ceqsexg  3182  elabgt  3194  elabgf  3195  axrep1  4532  axrep3  4534  axrep4  4535  copsex2t  4705  copsex2g  4706  opelopabsb  4728  opeliunxp2  4995  ralxpf  5003  cbviota  5574  sb8iota  5576  fvopab5  6002  fmptco  6085  nfiso  6245  dfoprab4f  6883  opeliunxp2f  6988  xpf1o  7765  zfcndrep  9070  gsumcom2  17662  isfildlem  20927  cnextfvval  21135  mbfsup  22676  mbfinf  22677  mbfinfOLD  22678  brabgaf  28269  fmptcof2  28311  bnj1468  29707  subtr2  31021  bj-abbi  31436  bj-axrep1  31449  bj-axrep3  31451  bj-axrep4  31452  mpt2bi123f  32452  dfcleqf  37471  fourierdlem31  38101  fourierdlem31OLD  38102
  Copyright terms: Public domain W3C validator