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

Theorem nfif 3968
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 3967 . 2  |-  ( T. 
->  F/_ x if (
ph ,  A ,  B ) )
87trud 1388 1  |-  F/_ x if ( ph ,  A ,  B )
Colors of variables: wff setvar class
Syntax hints:   T. wtru 1380   F/wnf 1599   F/_wnfc 2615   ifcif 3939
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-if 3940
This theorem is referenced by:  csbif  3989  csbifgOLD  3990  nfop  4229  nfrdg  7080  boxcutc  7512  nfoi  7939  nfsum1  13475  nfsum  13476  summolem2a  13500  zsum  13503  sumss  13509  sumss2  13511  fsumcvg2  13512  pcmpt  14270  pcmptdvds  14272  gsummpt1n0  16795  madugsum  18940  mbfpos  21821  mbfposb  21823  i1fposd  21877  isibl2  21936  nfitg  21944  cbvitg  21945  itgss3  21984  itgcn  22012  limcmpt  22050  rlimcnp2  23052  chirred  27018  nfcprod  28648  cbvprod  28652  prodmolem2a  28671  zprod  28674  fprod  28678  fprodntriv  28679  prodss  28684  refsum2cn  31019  ssfiunibd  31114  icccncfext  31254  fourierdlem86  31521  nfafv  31716  cdleme31sn  35194  cdleme32d  35258  cdleme32f  35260
  Copyright terms: Public domain W3C validator