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

Theorem nf3an 1774
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 1771 . . 3  |-  F/ x
( ph  /\  ps )
5 nf.3 . . 3  |-  F/ x ch
64, 5nfan 1771 . 2  |-  F/ x
( ( ph  /\  ps )  /\  ch )
71, 6nfxfr 1557 1  |-  F/ x
( ph  /\  ps  /\  ch )
Colors of variables: wff set class
Syntax hints:    /\ wa 358    /\ w3a 934   F/wnf 1531
This theorem is referenced by:  vtocl3gaf  2852  mob  2947  reusv6OLD  4545  infpssrlem4  7932  axcc3  8064  axdc3lem4  8079  axdc4lem  8081  axacndlem4  8232  axacndlem5  8233  axacnd  8234  mreexexd  13550  iuncon  17154  dedekind  23493  dedekindle  23494  dfon2lem1  23550  dfon2lem3  23552  upixp  25815  sdclem1  25865  rfcnnnub  27119  fmuldfeqlem1  27124  fmuldfeq  27125  fmul01lt1  27128  infrglb  27134  stoweidlem16  27177  stoweidlem17  27178  stoweidlem19  27180  stoweidlem20  27181  stoweidlem22  27183  stoweidlem26  27187  stoweidlem28  27189  stoweidlem31  27192  stoweidlem34  27195  stoweidlem35  27196  stoweidlem48  27209  stoweidlem51  27212  stoweidlem52  27213  stoweidlem53  27214  stoweidlem56  27217  stoweidlem57  27218  stoweidlem60  27221  tratrb  27672  bnj919  28170  bnj1379  28236  bnj571  28311  bnj607  28321  bnj873  28329  bnj964  28348  bnj981  28355  bnj1123  28389  bnj1128  28393  bnj1204  28415  bnj1279  28421  bnj1388  28436  bnj1398  28437  bnj1417  28444  bnj1444  28446  bnj1445  28447  bnj1449  28451  bnj1489  28459  bnj1518  28467  bnj1525  28472  pmapglbx  29331  cdlemefr29exN  29964
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936  df-tru 1310  df-nf 1532
  Copyright terms: Public domain W3C validator