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

Theorem nfbi 1906
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 1905 . 2 (⊤ → Ⅎ𝑥(𝜑𝜓))
65mptru 1546 1 𝑥(𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 205  wtru 1540  wnf 1786
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-nf 1787
This theorem is referenced by:  sbbib  2359  euf  2576  sb8eulem  2598  axextmo  2713  abbi  2810  cleqh  2862  cleqf  2938  sbhypf  3491  ceqsexg  3583  elabgtOLD  3604  elabgf  3605  elabgOLD  3608  axrep1  5210  axrep3  5213  axrep4  5214  copsex2t  5406  copsex2gOLD  5408  opeliunxp2  5747  ralxpf  5755  cbviotaw  6398  cbviota  6401  sb8iota  6403  fvopab5  6907  fmptco  7001  nfiso  7193  dfoprab4f  7896  opeliunxp2f  8026  xpf1o  8926  zfcndrep  10370  gsumcom2  19576  isfildlem  23008  cnextfvval  23216  mbfsup  24828  mbfinf  24829  brabgaf  30948  fmptcof2  30994  bnj1468  32826  subtr2  34504  mpobi123f  36320  eqrelf  36395  fourierdlem31  43679
  Copyright terms: Public domain W3C validator