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

Theorem nfbi 1903
 Description: If 𝑥 is not free in 𝜑 and 𝜓, then it is not free in (𝜑 ↔ 𝜓). (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 𝑥𝜑
nf.2 𝑥𝜓
Assertion
Ref Expression
nfbi 𝑥(𝜑𝜓)

Proof of Theorem nfbi
StepHypRef Expression
1 nf.1 . . . 4 𝑥𝜑
21a1i 11 . . 3 (⊤ → Ⅎ𝑥𝜑)
3 nf.2 . . . 4 𝑥𝜓
43a1i 11 . . 3 (⊤ → Ⅎ𝑥𝜓)
52, 4nfbid 1902 . 2 (⊤ → Ⅎ𝑥(𝜑𝜓))
65mptru 1543 1 𝑥(𝜑𝜓)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 208  ⊤wtru 1537  Ⅎwnf 1783 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784 This theorem is referenced by:  sbbibOLD  2288  sbbib  2379  euf  2660  sb8eulem  2683  axextmo  2800  abbi  2891  cleqh  2939  cleqf  3013  sbhypf  3555  ceqsexg  3649  elabgt  3666  elabgf  3667  elabg  3669  axrep1  5194  axrep3  5197  axrep4  5198  copsex2t  5386  copsex2g  5387  opelopabsb  5420  opeliunxp2  5712  ralxpf  5720  cbviotaw  6324  cbviota  6326  sb8iota  6328  fvopab5  6803  fmptco  6894  nfiso  7078  dfoprab4f  7757  opeliunxp2f  7879  xpf1o  8682  zfcndrep  10039  gsumcom2  19098  isfildlem  22468  cnextfvval  22676  mbfsup  24268  mbfinf  24269  brabgaf  30362  fmptcof2  30405  bnj1468  32122  subtr2  33667  mpobi123f  35444  eqrelf  35521  fourierdlem31  42430  dfich2OLD  43623
 Copyright terms: Public domain W3C validator