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

Theorem nf3an 1861
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 960 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ps )  /\  ch )
)
2 nfan.1 . . . 4  |-  F/ x ph
3 nfan.2 . . . 4  |-  F/ x ps
42, 3nfan 1859 . . 3  |-  F/ x
( ph  /\  ps )
5 nfan.3 . . 3  |-  F/ x ch
64, 5nfan 1859 . 2  |-  F/ x
( ( ph  /\  ps )  /\  ch )
71, 6nfxfr 1618 1  |-  F/ x
( ph  /\  ps  /\  ch )
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369    /\ w3a 958   F/wnf 1592
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 960  df-ex 1590  df-nf 1593
This theorem is referenced by:  hb3an  1863  vtocl3gaf  3028  mob  3130  reusv6OLD  4491  infpssrlem4  8463  axcc3  8595  axdc3lem4  8610  axdc4lem  8612  axacndlem4  8764  axacndlem5  8765  axacnd  8766  dedekind  9520  dedekindle  9521  mreexexd  14568  gsummatr01lem4  18305  iuncon  18873  hasheuni  26387  measvunilem  26479  measvunilem0  26480  measvuni  26481  volfiniune  26499  nfcprod1  27269  nfcprod  27270  dfon2lem1  27442  dfon2lem3  27444  nfwrecs  27565  upixp  28464  sdclem1  28480  rfcnnnub  29600  fmuldfeqlem1  29605  fmuldfeq  29606  fmul01lt1  29609  infrglb  29614  stoweidlem16  29654  stoweidlem17  29655  stoweidlem19  29657  stoweidlem20  29658  stoweidlem22  29660  stoweidlem26  29664  stoweidlem28  29666  stoweidlem31  29669  stoweidlem34  29672  stoweidlem35  29673  stoweidlem48  29686  stoweidlem52  29690  stoweidlem53  29691  stoweidlem56  29694  stoweidlem57  29695  stoweidlem60  29698  ovmpt3rab1  30004  tratrb  30940  bnj919  31459  bnj1379  31523  bnj571  31598  bnj607  31608  bnj873  31616  bnj964  31635  bnj981  31642  bnj1123  31676  bnj1128  31680  bnj1204  31702  bnj1279  31708  bnj1388  31723  bnj1398  31724  bnj1417  31731  bnj1444  31733  bnj1445  31734  bnj1449  31738  bnj1489  31746  bnj1518  31754  bnj1525  31759  pmapglbx  32983  cdlemefr29exN  33616
  Copyright terms: Public domain W3C validator