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

Theorem nfif 3602
Description: Bound-variable hypothesis builder for a conditional operator. (Contributed by NM, 16-Feb-2005.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
Hypotheses
Ref Expression
nfif.1  |-  F/ x ph
nfif.2  |-  F/_ x A
nfif.3  |-  F/_ x B
Assertion
Ref Expression
nfif  |-  F/_ x if ( ph ,  A ,  B )

Proof of Theorem nfif
StepHypRef Expression
1 nfif.1 . . . 4  |-  F/ x ph
21a1i 10 . . 3  |-  (  T. 
->  F/ x ph )
3 nfif.2 . . . 4  |-  F/_ x A
43a1i 10 . . 3  |-  (  T. 
->  F/_ x A )
5 nfif.3 . . . 4  |-  F/_ x B
65a1i 10 . . 3  |-  (  T. 
->  F/_ x B )
72, 4, 6nfifd 3601 . 2  |-  (  T. 
->  F/_ x if (
ph ,  A ,  B ) )
87trud 1314 1  |-  F/_ x if ( ph ,  A ,  B )
Colors of variables: wff set class
Syntax hints:    T. wtru 1307   F/wnf 1534   F/_wnfc 2419   ifcif 3578
This theorem is referenced by:  csbifg  3606  nfop  3828  nfriota1  6328  nfrdg  6443  boxcutc  6875  nfoi  7245  nfsum  12180  cbvsum  12184  summolem2a  12204  zsum  12207  fsum  12209  sumss  12213  sumss2  12215  fsumcvg2  12216  pcmpt  12956  pcmptdvds  12958  mbfpos  19022  mbfposb  19024  i1fposd  19078  isibl2  19137  nfitg  19145  cbvitg  19146  itgss3  19185  itgcn  19213  limcmpt  19249  rlimcnp2  20277  chirred  22991  nfcprod  24133  cbvcprod  24137  prodmolem2a  24157  zprod  24160  fprod  24164  itgaddnclem2  25010  nfprod1  25413  nfprod  25414  refsum2cn  27812  nfafv  28104  cdleme31sn  31191  cdleme32d  31255  cdleme32f  31257
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-if 3579
  Copyright terms: Public domain W3C validator