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

Theorem nf3an 1895
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 1083 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
2 nfan.1 . . . 4 𝑥𝜑
3 nfan.2 . . . 4 𝑥𝜓
42, 3nfan 1893 . . 3 𝑥(𝜑𝜓)
5 nfan.3 . . 3 𝑥𝜒
64, 5nfan 1893 . 2 𝑥((𝜑𝜓) ∧ 𝜒)
71, 6nfxfr 1846 1 𝑥(𝜑𝜓𝜒)
Colors of variables: wff setvar class
Syntax hints:  wa 396  w3a 1081  wnf 1777
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778
This theorem is referenced by:  hb3an  2303  vtocl3gaf  3581  mob  3711  nfwrecs  7943  infpssrlem4  9720  axcc3  9852  axdc3lem4  9867  axdc4lem  9869  axacndlem4  10024  axacndlem5  10025  axacnd  10026  dedekind  10795  dedekindle  10796  nfcprod1  15256  nfcprod  15257  fprodle  15342  mreexexd  16911  gsumsnf  18995  gsummatr01lem4  21183  iunconn  21952  hasheuni  31231  measvunilem  31358  measvunilem0  31359  measvuni  31360  volfiniune  31376  bnj919  31925  bnj1379  31989  bnj571  32065  bnj607  32075  bnj873  32083  bnj964  32102  bnj981  32109  bnj1123  32143  bnj1128  32147  bnj1204  32169  bnj1279  32175  bnj1388  32190  bnj1398  32191  bnj1417  32198  bnj1444  32200  bnj1445  32201  bnj1449  32205  bnj1489  32213  bnj1518  32221  bnj1525  32226  dfon2lem1  32913  dfon2lem3  32915  nffrecs  33005  isbasisrelowllem1  34506  isbasisrelowllem2  34507  poimirlem27  34787  upixp  34873  sdclem1  34887  pmapglbx  36773  cdlemefr29exN  37406  gneispace  40346  tratrb  40732  rfcnnnub  41155  uzwo4  41177  suprnmpt  41292  choicefi  41325  iunmapsn  41342  infxr  41497  rexabslelem  41554  fsumiunss  41718  fmuldfeqlem1  41725  fmuldfeq  41726  fmul01lt1  41729  mullimc  41759  mullimcf  41766  limsupre  41784  addlimc  41791  0ellimcdiv  41792  fnlimfvre  41817  climinf2mpt  41857  climinfmpt  41858  limsupmnfuzlem  41869  dvmptfprodlem  42091  dvmptfprod  42092  dvnprodlem1  42093  iblspltprt  42120  stoweidlem16  42164  stoweidlem17  42165  stoweidlem19  42167  stoweidlem20  42168  stoweidlem22  42170  stoweidlem26  42174  stoweidlem28  42176  stoweidlem31  42179  stoweidlem34  42182  stoweidlem35  42183  stoweidlem48  42196  stoweidlem52  42200  stoweidlem53  42201  stoweidlem56  42204  stoweidlem57  42205  stoweidlem60  42208  fourierdlem73  42327  fourierdlem77  42331  fourierdlem83  42337  fourierdlem87  42341  etransclem32  42414  sge0pnffigt  42541  sge0iunmptlemre  42560  sge0iunmpt  42563  meaiininc2  42633  opnvonmbllem2  42778  issmfle  42885  issmfgt  42896  issmfge  42909  smflimlem2  42911  smflimmpt  42947  smfinflem  42954  smflimsuplem7  42963  smflimsuplem8  42964  smflimsupmpt  42966  smfliminfmpt  42969  ich2exprop  43462  ichnreuop  43463
  Copyright terms: Public domain W3C validator