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

Theorem nfbi 1935
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 1934 . 2  |-  ( T. 
->  F/ x ( ph  <->  ps ) )
65trud 1404 1  |-  F/ x
( ph  <->  ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184   T. wtru 1396   F/wnf 1617
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-12 1855
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618
This theorem is referenced by:  euf  2293  sb8eu  2319  sb8euOLD  2320  bm1.1  2440  bm1.1OLD  2441  cleqh  2572  abbiOLD  2589  nfeqOLD  2631  cleqfOLD  2647  sbhypf  3156  ceqsexg  3231  elabgt  3243  elabgf  3244  axrep1  4569  axrep3  4571  axrep4  4572  copsex2t  4743  copsex2g  4744  opelopabsb  4766  opeliunxp2  5151  ralxpf  5159  cbviota  5562  sb8iota  5564  fvopab5  5980  fmptco  6065  nfiso  6221  dfoprab4f  6857  xpf1o  7698  zfcndrep  9009  uzindOLD  10978  gsumcom2  17129  isfildlem  20483  cnextfvval  20690  mbfsup  22196  mbfinf  22197  brabgaf  27599  fmptcof2  27645  subtr2  30295  mpt2bi123f  30733  fourierdlem31  32081  bnj1468  34005  bj-abbi  34462  bj-axrep1  34475  bj-axrep3  34477  bj-axrep4  34478
  Copyright terms: Public domain W3C validator