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

Theorem nf3an 1871
Description: If 𝑥 is not free in 𝜑, 𝜓, and 𝜒, 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 1056 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
2 nfan.1 . . . 4 𝑥𝜑
3 nfan.2 . . . 4 𝑥𝜓
42, 3nfan 1868 . . 3 𝑥(𝜑𝜓)
5 nfan.3 . . 3 𝑥𝜒
64, 5nfan 1868 . 2 𝑥((𝜑𝜓) ∧ 𝜒)
71, 6nfxfr 1819 1 𝑥(𝜑𝜓𝜒)
Colors of variables: wff setvar class
Syntax hints:  wa 383  w3a 1054  wnf 1748
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750
This theorem is referenced by:  hb3an  2167  vtocl3gaf  3306  mob  3421  nfwrecs  7454  infpssrlem4  9166  axcc3  9298  axdc3lem4  9313  axdc4lem  9315  axacndlem4  9470  axacndlem5  9471  axacnd  9472  dedekind  10238  dedekindle  10239  nfcprod1  14684  nfcprod  14685  fprodle  14771  mreexexd  16355  mreexexdOLD  16356  gsumsnf  18399  gsummatr01lem4  20512  iunconn  21279  hasheuni  30275  measvunilem  30403  measvunilem0  30404  measvuni  30405  volfiniune  30421  bnj919  30963  bnj1379  31027  bnj571  31102  bnj607  31112  bnj873  31120  bnj964  31139  bnj981  31146  bnj1123  31180  bnj1128  31184  bnj1204  31206  bnj1279  31212  bnj1388  31227  bnj1398  31228  bnj1417  31235  bnj1444  31237  bnj1445  31238  bnj1449  31242  bnj1489  31250  bnj1518  31258  bnj1525  31263  dfon2lem1  31812  dfon2lem3  31814  nffrecs  31903  isbasisrelowllem1  33333  isbasisrelowllem2  33334  poimirlem27  33566  upixp  33654  sdclem1  33669  pmapglbx  35373  cdlemefr29exN  36007  gneispace  38749  tratrb  39063  rfcnnnub  39509  uzwo4  39535  suprnmpt  39669  wessf1ornlem  39685  choicefi  39706  iunmapsn  39723  infxr  39896  rexabslelem  39958  fsumiunss  40125  fmuldfeqlem1  40132  fmuldfeq  40133  fmul01lt1  40136  mullimc  40166  mullimcf  40173  limsupre  40191  addlimc  40198  0ellimcdiv  40199  fnlimfvre  40224  climinf2mpt  40264  climinfmpt  40265  limsupmnfuzlem  40276  dvmptfprodlem  40477  dvmptfprod  40478  dvnprodlem1  40479  iblspltprt  40507  stoweidlem16  40551  stoweidlem17  40552  stoweidlem19  40554  stoweidlem20  40555  stoweidlem22  40557  stoweidlem26  40561  stoweidlem28  40563  stoweidlem31  40566  stoweidlem34  40569  stoweidlem35  40570  stoweidlem48  40583  stoweidlem52  40587  stoweidlem53  40588  stoweidlem56  40591  stoweidlem57  40592  stoweidlem60  40595  fourierdlem73  40714  fourierdlem77  40718  fourierdlem83  40724  fourierdlem87  40728  etransclem32  40801  sge0pnffigt  40931  sge0iunmptlemre  40950  sge0iunmpt  40953  meaiininc2  41023  opnvonmbllem2  41168  issmfle  41275  issmfgt  41286  issmfge  41299  smflimlem2  41301  smflimmpt  41337  smfinflem  41344  smflimsuplem7  41353  smflimsuplem8  41354  smflimsupmpt  41356  smfliminfmpt  41359
  Copyright terms: Public domain W3C validator