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

Theorem nf3an 1786
Description: If  x is not free in  ph,  ps, and  ch, it is not free in  ( ph  /\  ps  /\  ch ). (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypotheses
Ref Expression
nf.1  |-  F/ x ph
nf.2  |-  F/ x ps
nf.3  |-  F/ x ch
Assertion
Ref Expression
nf3an  |-  F/ x
( ph  /\  ps  /\  ch )

Proof of Theorem nf3an
StepHypRef Expression
1 df-3an 936 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ps )  /\  ch )
)
2 nf.1 . . . 4  |-  F/ x ph
3 nf.2 . . . 4  |-  F/ x ps
42, 3nfan 1783 . . 3  |-  F/ x
( ph  /\  ps )
5 nf.3 . . 3  |-  F/ x ch
64, 5nfan 1783 . 2  |-  F/ x
( ( ph  /\  ps )  /\  ch )
71, 6nfxfr 1560 1  |-  F/ x
( ph  /\  ps  /\  ch )
Colors of variables: wff set class
Syntax hints:    /\ wa 358    /\ w3a 934   F/wnf 1534
This theorem is referenced by:  vtocl3gaf  2865  mob  2960  reusv6OLD  4561  infpssrlem4  7948  axcc3  8080  axdc3lem4  8095  axdc4lem  8097  axacndlem4  8248  axacndlem5  8249  axacnd  8250  mreexexd  13566  iuncon  17170  hasheuni  23468  measvunilem  23555  measvunilem0  23556  measvuni  23557  dedekind  24097  dedekindle  24098  nfcprod1  24132  nfcprod  24133  dfon2lem1  24210  dfon2lem3  24212  upixp  26506  sdclem1  26556  rfcnnnub  27810  fmuldfeqlem1  27815  fmuldfeq  27816  fmul01lt1  27819  infrglb  27825  stoweidlem16  27868  stoweidlem17  27869  stoweidlem19  27871  stoweidlem20  27872  stoweidlem22  27874  stoweidlem26  27878  stoweidlem28  27880  stoweidlem31  27883  stoweidlem34  27886  stoweidlem35  27887  stoweidlem48  27900  stoweidlem51  27903  stoweidlem52  27904  stoweidlem53  27905  stoweidlem56  27908  stoweidlem57  27909  stoweidlem60  27912  tratrb  28598  bnj919  29113  bnj1379  29179  bnj571  29254  bnj607  29264  bnj873  29272  bnj964  29291  bnj981  29298  bnj1123  29332  bnj1128  29336  bnj1204  29358  bnj1279  29364  bnj1388  29379  bnj1398  29380  bnj1417  29387  bnj1444  29389  bnj1445  29390  bnj1449  29394  bnj1489  29402  bnj1518  29410  bnj1525  29415  pmapglbx  30580  cdlemefr29exN  31213
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936  df-tru 1310  df-nf 1535
  Copyright terms: Public domain W3C validator