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

Theorem nfbid 1902
Description: If in a context 𝑥 is not free in 𝜓 and 𝜒, then it is not free in (𝜓𝜒). (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 29-Dec-2017.)
Hypotheses
Ref Expression
nfbid.1 (𝜑 → Ⅎ𝑥𝜓)
nfbid.2 (𝜑 → Ⅎ𝑥𝜒)
Assertion
Ref Expression
nfbid (𝜑 → Ⅎ𝑥(𝜓𝜒))

Proof of Theorem nfbid
StepHypRef Expression
1 dfbi2 474 . 2 ((𝜓𝜒) ↔ ((𝜓𝜒) ∧ (𝜒𝜓)))
2 nfbid.1 . . . 4 (𝜑 → Ⅎ𝑥𝜓)
3 nfbid.2 . . . 4 (𝜑 → Ⅎ𝑥𝜒)
42, 3nfimd 1894 . . 3 (𝜑 → Ⅎ𝑥(𝜓𝜒))
53, 2nfimd 1894 . . 3 (𝜑 → Ⅎ𝑥(𝜒𝜓))
64, 5nfand 1897 . 2 (𝜑 → Ⅎ𝑥((𝜓𝜒) ∧ (𝜒𝜓)))
71, 6nfxfrd 1854 1 (𝜑 → Ⅎ𝑥(𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  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 207  df-an 396  df-or 849  df-ex 1780  df-nf 1784
This theorem is referenced by:  nfbi  1903  nfeqd  2916  nfiotadw  6517  nfiotad  6519  iota2df  6548  axextnd  10631  axrepndlem1  10632  axrepndlem2  10633  axacndlem4  10650  axacndlem5  10651  axacnd  10652  axsepg2  35096  axsepg2ALT  35097  axextdist  35800  copsex2d  37140  cbveud  37373  wl-eudf  37573  wl-sb8eut  37579  wl-sb8eutv  37580
  Copyright terms: Public domain W3C validator