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

Theorem nf3an 1909
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 1091 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
2 nfan.1 . . . 4 𝑥𝜑
3 nfan.2 . . . 4 𝑥𝜓
42, 3nfan 1907 . . 3 𝑥(𝜑𝜓)
5 nfan.3 . . 3 𝑥𝜒
64, 5nfan 1907 . 2 𝑥((𝜑𝜓) ∧ 𝜒)
71, 6nfxfr 1860 1 𝑥(𝜑𝜓𝜒)
Colors of variables: wff setvar class
Syntax hints:  wa 399  w3a 1089  wnf 1791
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-ex 1788  df-nf 1792
This theorem is referenced by:  hb3an  2304  vtocl3gaf  3507  mob  3647  nffrecs  8048  nfwrecs  8072  infpssrlem4  9949  axcc3  10081  axdc3lem4  10096  axdc4lem  10098  axacndlem4  10253  axacndlem5  10254  axacnd  10255  dedekind  11024  dedekindle  11025  nfcprod1  15504  nfcprod  15505  fprodle  15590  mreexexd  17183  gsumsnf  19370  gsummatr01lem4  21586  iunconn  22356  hasheuni  31796  measvunilem  31923  measvunilem0  31924  measvuni  31925  volfiniune  31941  bnj919  32490  bnj1379  32553  bnj571  32629  bnj607  32639  bnj873  32647  bnj964  32666  bnj981  32673  bnj1123  32709  bnj1128  32713  bnj1204  32735  bnj1279  32741  bnj1388  32756  bnj1398  32757  bnj1417  32764  bnj1444  32766  bnj1445  32767  bnj1449  32771  bnj1489  32779  bnj1518  32787  bnj1525  32792  dfon2lem1  33508  dfon2lem3  33510  isbasisrelowllem1  35299  isbasisrelowllem2  35300  poimirlem27  35577  upixp  35660  sdclem1  35674  pmapglbx  37556  cdlemefr29exN  38189  gneispace  41468  tratrb  41876  rfcnnnub  42299  uzwo4  42321  suprnmpt  42430  choicefi  42460  iunmapsn  42477  infxr  42626  rexabslelem  42678  fsumiunss  42836  fmuldfeqlem1  42843  fmuldfeq  42844  fmul01lt1  42847  mullimc  42877  mullimcf  42884  limsupre  42902  addlimc  42909  0ellimcdiv  42910  fnlimfvre  42935  climinf2mpt  42975  climinfmpt  42976  limsupmnfuzlem  42987  dvmptfprodlem  43205  dvmptfprod  43206  dvnprodlem1  43207  iblspltprt  43234  stoweidlem16  43277  stoweidlem17  43278  stoweidlem19  43280  stoweidlem20  43281  stoweidlem22  43283  stoweidlem26  43287  stoweidlem28  43289  stoweidlem31  43292  stoweidlem34  43295  stoweidlem35  43296  stoweidlem48  43309  stoweidlem52  43313  stoweidlem53  43314  stoweidlem56  43317  stoweidlem57  43318  stoweidlem60  43321  fourierdlem73  43440  fourierdlem77  43444  fourierdlem83  43450  fourierdlem87  43454  etransclem32  43527  sge0pnffigt  43654  sge0iunmptlemre  43673  sge0iunmpt  43676  meaiininc2  43746  opnvonmbllem2  43891  issmfle  43998  issmfgt  44009  issmfge  44022  smflimlem2  44024  smflimmpt  44060  smfinflem  44067  smflimsuplem7  44076  smflimsuplem8  44077  smflimsupmpt  44079  smfliminfmpt  44082  ich2exprop  44641  ichnreuop  44642  2arymaptfo  45718
  Copyright terms: Public domain W3C validator