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

Theorem nfif 3944
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 11 . . 3  |-  ( T. 
->  F/ x ph )
3 nfif.2 . . . 4  |-  F/_ x A
43a1i 11 . . 3  |-  ( T. 
->  F/_ x A )
5 nfif.3 . . . 4  |-  F/_ x B
65a1i 11 . . 3  |-  ( T. 
->  F/_ x B )
72, 4, 6nfifd 3943 . 2  |-  ( T. 
->  F/_ x if (
ph ,  A ,  B ) )
87trud 1446 1  |-  F/_ x if ( ph ,  A ,  B )
Colors of variables: wff setvar class
Syntax hints:   T. wtru 1438   F/wnf 1663   F/_wnfc 2577   ifcif 3915
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-if 3916
This theorem is referenced by:  csbif  3965  nfop  4206  nfrdg  7140  boxcutc  7573  nfoi  8029  nfsum1  13734  nfsum  13735  summolem2a  13759  zsum  13762  sumss  13768  sumss2  13770  fsumcvg2  13771  nfcprod  13943  cbvprod  13947  prodmolem2a  13966  zprod  13969  fprod  13973  fprodntriv  13974  prodss  13979  pcmpt  14800  pcmptdvds  14802  gsummpt1n0  17536  madugsum  19603  mbfpos  22492  mbfposb  22494  i1fposd  22550  isibl2  22609  nfitg  22617  cbvitg  22618  itgss3  22657  itgcn  22685  limcmpt  22723  rlimcnp2  23765  chirred  27891  cdleme31sn  33667  cdleme32d  33731  cdleme32f  33733  refsum2cn  37014  ssfiunibd  37151  icccncfext  37352  fourierdlem86  37639  nfafv  38052
  Copyright terms: Public domain W3C validator