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

Theorem nf3an 2001
Description: If 𝑥 is not free in 𝜑, 𝜓, and 𝜒, then it is not free in (𝜑𝜓𝜒). (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypotheses
Ref Expression
nfan.1 𝑥𝜑
nfan.2 𝑥𝜓
nfan.3 𝑥𝜒
Assertion
Ref Expression
nf3an 𝑥(𝜑𝜓𝜒)

Proof of Theorem nf3an
StepHypRef Expression
1 df-3an 1110 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
2 nfan.1 . . . 4 𝑥𝜑
3 nfan.2 . . . 4 𝑥𝜓
42, 3nfan 1999 . . 3 𝑥(𝜑𝜓)
5 nfan.3 . . 3 𝑥𝜒
64, 5nfan 1999 . 2 𝑥((𝜑𝜓) ∧ 𝜒)
71, 6nfxfr 1949 1 𝑥(𝜑𝜓𝜒)
Colors of variables: wff setvar class
Syntax hints:  wa 385  w3a 1108  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-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880
This theorem is referenced by:  hb3an  2325  vtocl3gaf  3461  mob  3582  nfwrecs  7645  infpssrlem4  9414  axcc3  9546  axdc3lem4  9561  axdc4lem  9563  axacndlem4  9718  axacndlem5  9719  axacnd  9720  dedekind  10488  dedekindle  10489  nfcprod1  14973  nfcprod  14974  fprodle  15059  mreexexd  16619  gsumsnf  18664  gsummatr01lem4  20787  iunconn  21556  hasheuni  30654  measvunilem  30782  measvunilem0  30783  measvuni  30784  volfiniune  30800  bnj919  31345  bnj1379  31409  bnj571  31484  bnj607  31494  bnj873  31502  bnj964  31521  bnj981  31528  bnj1123  31562  bnj1128  31566  bnj1204  31588  bnj1279  31594  bnj1388  31609  bnj1398  31610  bnj1417  31617  bnj1444  31619  bnj1445  31620  bnj1449  31624  bnj1489  31632  bnj1518  31640  bnj1525  31645  dfon2lem1  32191  dfon2lem3  32193  nffrecs  32282  isbasisrelowllem1  33692  isbasisrelowllem2  33693  poimirlem27  33916  upixp  34003  sdclem1  34017  pmapglbx  35781  cdlemefr29exN  36414  gneispace  39201  tratrb  39509  rfcnnnub  39942  uzwo4  39967  suprnmpt  40097  wessf1ornlem  40112  choicefi  40131  iunmapsn  40148  infxr  40314  rexabslelem  40375  fsumiunss  40538  fmuldfeqlem1  40545  fmuldfeq  40546  fmul01lt1  40549  mullimc  40579  mullimcf  40586  limsupre  40604  addlimc  40611  0ellimcdiv  40612  fnlimfvre  40637  climinf2mpt  40677  climinfmpt  40678  limsupmnfuzlem  40689  dvmptfprodlem  40890  dvmptfprod  40891  dvnprodlem1  40892  iblspltprt  40919  stoweidlem16  40963  stoweidlem17  40964  stoweidlem19  40966  stoweidlem20  40967  stoweidlem22  40969  stoweidlem26  40973  stoweidlem28  40975  stoweidlem31  40978  stoweidlem34  40981  stoweidlem35  40982  stoweidlem48  40995  stoweidlem52  40999  stoweidlem53  41000  stoweidlem56  41003  stoweidlem57  41004  stoweidlem60  41007  fourierdlem73  41126  fourierdlem77  41130  fourierdlem83  41136  fourierdlem87  41140  etransclem32  41213  sge0pnffigt  41343  sge0iunmptlemre  41362  sge0iunmpt  41365  meaiininc2  41435  opnvonmbllem2  41580  issmfle  41687  issmfgt  41698  issmfge  41711  smflimlem2  41713  smflimmpt  41749  smfinflem  41756  smflimsuplem7  41765  smflimsuplem8  41766  smflimsupmpt  41768  smfliminfmpt  41771
  Copyright terms: Public domain W3C validator