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

Theorem nf3an 1893
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 1081 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
2 nfan.1 . . . 4 𝑥𝜑
3 nfan.2 . . . 4 𝑥𝜓
42, 3nfan 1891 . . 3 𝑥(𝜑𝜓)
5 nfan.3 . . 3 𝑥𝜒
64, 5nfan 1891 . 2 𝑥((𝜑𝜓) ∧ 𝜒)
71, 6nfxfr 1844 1 𝑥(𝜑𝜓𝜒)
Colors of variables: wff setvar class
Syntax hints:  wa 396  w3a 1079  wnf 1775
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776
This theorem is referenced by:  hb3an  2301  vtocl3gaf  3577  mob  3707  nfwrecs  7940  infpssrlem4  9717  axcc3  9849  axdc3lem4  9864  axdc4lem  9866  axacndlem4  10021  axacndlem5  10022  axacnd  10023  dedekind  10792  dedekindle  10793  nfcprod1  15254  nfcprod  15255  fprodle  15340  mreexexd  16909  gsumsnf  19004  gsummatr01lem4  21197  iunconn  21966  hasheuni  31244  measvunilem  31371  measvunilem0  31372  measvuni  31373  volfiniune  31389  bnj919  31938  bnj1379  32002  bnj571  32078  bnj607  32088  bnj873  32096  bnj964  32115  bnj981  32122  bnj1123  32156  bnj1128  32160  bnj1204  32182  bnj1279  32188  bnj1388  32203  bnj1398  32204  bnj1417  32211  bnj1444  32213  bnj1445  32214  bnj1449  32218  bnj1489  32226  bnj1518  32234  bnj1525  32239  dfon2lem1  32926  dfon2lem3  32928  nffrecs  33018  isbasisrelowllem1  34519  isbasisrelowllem2  34520  poimirlem27  34801  upixp  34887  sdclem1  34901  pmapglbx  36787  cdlemefr29exN  37420  gneispace  40364  tratrb  40750  rfcnnnub  41173  uzwo4  41195  suprnmpt  41310  choicefi  41343  iunmapsn  41360  infxr  41515  rexabslelem  41572  fsumiunss  41736  fmuldfeqlem1  41743  fmuldfeq  41744  fmul01lt1  41747  mullimc  41777  mullimcf  41784  limsupre  41802  addlimc  41809  0ellimcdiv  41810  fnlimfvre  41835  climinf2mpt  41875  climinfmpt  41876  limsupmnfuzlem  41887  dvmptfprodlem  42109  dvmptfprod  42110  dvnprodlem1  42111  iblspltprt  42138  stoweidlem16  42182  stoweidlem17  42183  stoweidlem19  42185  stoweidlem20  42186  stoweidlem22  42188  stoweidlem26  42192  stoweidlem28  42194  stoweidlem31  42197  stoweidlem34  42200  stoweidlem35  42201  stoweidlem48  42214  stoweidlem52  42218  stoweidlem53  42219  stoweidlem56  42222  stoweidlem57  42223  stoweidlem60  42226  fourierdlem73  42345  fourierdlem77  42349  fourierdlem83  42355  fourierdlem87  42359  etransclem32  42432  sge0pnffigt  42559  sge0iunmptlemre  42578  sge0iunmpt  42581  meaiininc2  42651  opnvonmbllem2  42796  issmfle  42903  issmfgt  42914  issmfge  42927  smflimlem2  42929  smflimmpt  42965  smfinflem  42972  smflimsuplem7  42981  smflimsuplem8  42982  smflimsupmpt  42984  smfliminfmpt  42987  ich2exprop  43480  ichnreuop  43481
  Copyright terms: Public domain W3C validator