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

Theorem nf3an 1832
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
nfan.1  |-  F/ x ph
nfan.2  |-  F/ x ps
nfan.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 nfan.1 . . . 4  |-  F/ x ph
3 nfan.2 . . . 4  |-  F/ x ps
42, 3nfan 1829 . . 3  |-  F/ x
( ph  /\  ps )
5 nfan.3 . . 3  |-  F/ x ch
64, 5nfan 1829 . 2  |-  F/ x
( ( ph  /\  ps )  /\  ch )
71, 6nfxfr 1570 1  |-  F/ x
( ph  /\  ps  /\  ch )
Colors of variables: wff set class
Syntax hints:    /\ wa 358    /\ w3a 934   F/wnf 1544
This theorem is referenced by:  hb3an  1835  vtocl3gaf  2928  mob  3023  reusv6OLD  4624  infpssrlem4  8019  axcc3  8151  axdc3lem4  8166  axdc4lem  8168  axacndlem4  8319  axacndlem5  8320  axacnd  8321  mreexexd  13643  iuncon  17254  hasheuni  23741  measvunilem  23830  measvunilem0  23831  measvuni  23832  volfiniune  23850  dedekind  24488  dedekindle  24489  nfcprod1  24537  nfcprod  24538  dfon2lem1  24697  dfon2lem3  24699  upixp  25727  sdclem1  25777  rfcnnnub  27030  fmuldfeqlem1  27035  fmuldfeq  27036  fmul01lt1  27039  infrglb  27045  stoweidlem16  27088  stoweidlem17  27089  stoweidlem19  27091  stoweidlem20  27092  stoweidlem22  27094  stoweidlem26  27098  stoweidlem28  27100  stoweidlem31  27103  stoweidlem34  27106  stoweidlem35  27107  stoweidlem48  27120  stoweidlem51  27123  stoweidlem52  27124  stoweidlem53  27125  stoweidlem56  27128  stoweidlem57  27129  stoweidlem60  27132  tratrb  28027  bnj919  28542  bnj1379  28608  bnj571  28683  bnj607  28693  bnj873  28701  bnj964  28720  bnj981  28727  bnj1123  28761  bnj1128  28765  bnj1204  28787  bnj1279  28793  bnj1388  28808  bnj1398  28809  bnj1417  28816  bnj1444  28818  bnj1445  28819  bnj1449  28823  bnj1489  28831  bnj1518  28839  bnj1525  28844  pmapglbx  30010  cdlemefr29exN  30643
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936  df-ex 1542  df-nf 1545
  Copyright terms: Public domain W3C validator