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

Theorem nfbi 2003
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 2002 . 2 (⊤ → Ⅎ𝑥(𝜑𝜓))
65mptru 1661 1 𝑥(𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 198  wtru 1654  wnf 1879
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880
This theorem is referenced by:  euf  2615  eufOLD  2616  sb8eu  2652  axextmo  2782  bm1.1OLD  2783  cleqh  2901  sbhypf  3441  ceqsexg  3523  elabgt  3537  elabgf  3538  elabg  3540  axrep1  4965  axrep3  4968  axrep4  4969  copsex2t  5147  copsex2g  5148  opelopabsb  5181  opeliunxp2  5464  ralxpf  5472  cbviota  6069  sb8iota  6071  fvopab5  6535  fmptco  6623  nfiso  6800  dfoprab4f  7461  opeliunxp2f  7574  xpf1o  8364  zfcndrep  9724  gsumcom2  18689  isfildlem  21989  cnextfvval  22197  mbfsup  23772  mbfinf  23773  brabgaf  29937  fmptcof2  29976  bnj1468  31433  subtr2  32822  bj-abbi  33271  bj-axrep1  33284  bj-axrep3  33286  bj-axrep4  33287  mpt2bi123f  34457  eqrelf  34520  fourierdlem31  41098
  Copyright terms: Public domain W3C validator