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

Theorem nfbid 1900
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 1892 . . 3 (𝜑 → Ⅎ𝑥(𝜓𝜒))
53, 2nfimd 1892 . . 3 (𝜑 → Ⅎ𝑥(𝜒𝜓))
64, 5nfand 1895 . 2 (𝜑 → Ⅎ𝑥((𝜓𝜒) ∧ (𝜒𝜓)))
71, 6nfxfrd 1851 1 (𝜑 → Ⅎ𝑥(𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wnf 1780
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1777  df-nf 1781
This theorem is referenced by:  nfbi  1901  nfeqd  2914  nfiotadw  6519  nfiotad  6521  iota2df  6550  axextnd  10629  axrepndlem1  10630  axrepndlem2  10631  axacndlem4  10648  axacndlem5  10649  axacnd  10650  axsepg2  35075  axsepg2ALT  35076  axextdist  35781  copsex2d  37122  cbveud  37355  wl-eudf  37553  wl-sb8eut  37559  wl-sb8eutv  37560
  Copyright terms: Public domain W3C validator