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

Theorem nfif 3755
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 3754 . 2  |-  (  T. 
->  F/_ x if (
ph ,  A ,  B ) )
87trud 1332 1  |-  F/_ x if ( ph ,  A ,  B )
Colors of variables: wff set class
Syntax hints:    T. wtru 1325   F/wnf 1553   F/_wnfc 2558   ifcif 3731
This theorem is referenced by:  csbifg  3759  nfop  3992  nfriota1  6549  nfrdg  6664  boxcutc  7097  nfoi  7475  nfsum  12477  cbvsum  12481  summolem2a  12501  zsum  12504  fsum  12506  sumss  12510  sumss2  12512  fsumcvg2  12513  pcmpt  13253  pcmptdvds  13255  mbfpos  19535  mbfposb  19537  i1fposd  19591  isibl2  19650  nfitg  19658  cbvitg  19659  itgss3  19698  itgcn  19726  limcmpt  19762  rlimcnp2  20797  chirred  23890  nfcprod  25229  cbvprod  25233  prodmolem2a  25252  zprod  25255  fprod  25259  fprodntriv  25260  prodss  25265  refsum2cn  27676  nfafv  27967  cdleme31sn  31114  cdleme32d  31178  cdleme32f  31180
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-if 3732
  Copyright terms: Public domain W3C validator