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

Theorem nf3an 1845
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 1842 . . 3  |-  F/ x
( ph  /\  ps )
5 nfan.3 . . 3  |-  F/ x ch
64, 5nfan 1842 . 2  |-  F/ x
( ( ph  /\  ps )  /\  ch )
71, 6nfxfr 1576 1  |-  F/ x
( ph  /\  ps  /\  ch )
Colors of variables: wff set class
Syntax hints:    /\ wa 359    /\ w3a 936   F/wnf 1550
This theorem is referenced by:  hb3an  1848  vtocl3gaf  2980  mob  3076  reusv6OLD  4693  infpssrlem4  8142  axcc3  8274  axdc3lem4  8289  axdc4lem  8291  axacndlem4  8441  axacndlem5  8442  axacnd  8443  mreexexd  13828  iuncon  17444  hasheuni  24428  measvunilem  24519  measvunilem0  24520  measvuni  24521  volfiniune  24539  dedekind  25140  dedekindle  25141  nfcprod1  25189  nfcprod  25190  dfon2lem1  25353  dfon2lem3  25355  upixp  26321  sdclem1  26337  rfcnnnub  27574  fmuldfeqlem1  27579  fmuldfeq  27580  fmul01lt1  27583  infrglb  27589  stoweidlem16  27632  stoweidlem17  27633  stoweidlem19  27635  stoweidlem20  27636  stoweidlem22  27638  stoweidlem26  27642  stoweidlem28  27644  stoweidlem31  27647  stoweidlem34  27650  stoweidlem35  27651  stoweidlem48  27664  stoweidlem52  27668  stoweidlem53  27669  stoweidlem56  27672  stoweidlem57  27673  stoweidlem60  27676  tratrb  28331  bnj919  28842  bnj1379  28908  bnj571  28983  bnj607  28993  bnj873  29001  bnj964  29020  bnj981  29027  bnj1123  29061  bnj1128  29065  bnj1204  29087  bnj1279  29093  bnj1388  29108  bnj1398  29109  bnj1417  29116  bnj1444  29118  bnj1445  29119  bnj1449  29123  bnj1489  29131  bnj1518  29139  bnj1525  29144  pmapglbx  30251  cdlemefr29exN  30884
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938  df-ex 1548  df-nf 1551
  Copyright terms: Public domain W3C validator