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

Theorem nf3an 1849
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 938 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ps )  /\  ch )
)
2 nfan.1 . . . 4  |-  F/ x ph
3 nfan.2 . . . 4  |-  F/ x ps
42, 3nfan 1846 . . 3  |-  F/ x
( ph  /\  ps )
5 nfan.3 . . 3  |-  F/ x ch
64, 5nfan 1846 . 2  |-  F/ x
( ( ph  /\  ps )  /\  ch )
71, 6nfxfr 1579 1  |-  F/ x
( ph  /\  ps  /\  ch )
Colors of variables: wff set class
Syntax hints:    /\ wa 359    /\ w3a 936   F/wnf 1553
This theorem is referenced by:  hb3an  1852  vtocl3gaf  3020  mob  3116  reusv6OLD  4734  infpssrlem4  8186  axcc3  8318  axdc3lem4  8333  axdc4lem  8335  axacndlem4  8485  axacndlem5  8486  axacnd  8487  mreexexd  13873  iuncon  17491  hasheuni  24475  measvunilem  24566  measvunilem0  24567  measvuni  24568  volfiniune  24586  dedekind  25187  dedekindle  25188  nfcprod1  25236  nfcprod  25237  dfon2lem1  25410  dfon2lem3  25412  nfwrecs  25533  upixp  26431  sdclem1  26447  rfcnnnub  27683  fmuldfeqlem1  27688  fmuldfeq  27689  fmul01lt1  27692  infrglb  27698  stoweidlem16  27741  stoweidlem17  27742  stoweidlem19  27744  stoweidlem20  27745  stoweidlem22  27747  stoweidlem26  27751  stoweidlem28  27753  stoweidlem31  27756  stoweidlem34  27759  stoweidlem35  27760  stoweidlem48  27773  stoweidlem52  27777  stoweidlem53  27778  stoweidlem56  27781  stoweidlem57  27782  stoweidlem60  27785  tratrb  28620  bnj919  29136  bnj1379  29202  bnj571  29277  bnj607  29287  bnj873  29295  bnj964  29314  bnj981  29321  bnj1123  29355  bnj1128  29359  bnj1204  29381  bnj1279  29387  bnj1388  29402  bnj1398  29403  bnj1417  29410  bnj1444  29412  bnj1445  29413  bnj1449  29417  bnj1489  29425  bnj1518  29433  bnj1525  29438  pmapglbx  30566  cdlemefr29exN  31199
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938  df-ex 1551  df-nf 1554
  Copyright terms: Public domain W3C validator