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

Theorem nfbi 1881
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 1880 . 2  |-  ( T. 
->  F/ x ( ph  <->  ps ) )
65trud 1388 1  |-  F/ x
( ph  <->  ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184   T. wtru 1380   F/wnf 1599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-12 1803
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600
This theorem is referenced by:  euf  2285  eufOLD  2286  sb8eu  2314  sb8euOLD  2315  sb8euOLDOLD  2316  bm1.1  2450  bm1.1OLD  2451  cleqh  2582  abbiOLD  2599  nfeqOLD  2641  cleqfOLD  2657  sbhypf  3160  ceqsexg  3235  elabgt  3247  elabgf  3248  axrep1  4559  axrep3  4561  axrep4  4562  copsex2t  4734  copsex2g  4735  opelopabsb  4757  opeliunxp2  5141  ralxpf  5149  cbviota  5556  sb8iota  5558  fvopab5  5974  fmptco  6055  nfiso  6209  dfoprab4f  6843  xpf1o  7680  zfcndrep  8993  uzindOLD  10956  gsumcom2  16818  isfildlem  20185  cnextfvval  20392  mbfsup  21898  mbfinf  21899  fmptcof2  27271  subtr2  29986  sbcalf  30347  sbcexf  30348  mpt2bi123f  30402  fourierdlem31  31665  bnj1468  33200  bj-abbi  33659  bj-axrep1  33672  bj-axrep3  33674  bj-axrep4  33675
  Copyright terms: Public domain W3C validator