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

Theorem nfbi 1846
Description: If  x is not free in  ph and  ps, 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
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 1844 . 2  |-  (  T. 
->  F/ x ( ph  <->  ps ) )
65trud 1329 1  |-  F/ x
( ph  <->  ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    T. wtru 1322   F/wnf 1550
This theorem is referenced by:  euf  2245  sb8eu  2257  bm1.1  2373  abbi  2498  nfeq  2531  cleqf  2548  sbhypf  2945  ceqsexg  3011  elabgt  3023  elabgf  3024  axrep1  4263  axrep3  4265  axrep4  4266  copsex2t  4385  copsex2g  4386  opelopabsb  4407  opeliunxp2  4954  ralxpf  4960  cbviota  5364  sb8iota  5366  fmptco  5841  nfiso  5984  dfoprab4f  6345  fvopab5  6471  xpf1o  7206  zfcndrep  8423  uzindOLD  10297  gsumcom2  15477  isfildlem  17811  cnextfvval  18018  mbfsup  19424  mbfinf  19425  fmptcof2  23919  subtr2  26010  bnj1468  28556
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-11 1753
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551
  Copyright terms: Public domain W3C validator