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

Theorem nfif 3589
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 3588 . 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 1531   F/_wnfc 2406   ifcif 3565
This theorem is referenced by:  csbifg  3593  nfop  3812  nfriota1  6312  nfrdg  6427  boxcutc  6859  nfoi  7229  nfsum  12164  cbvsum  12168  summolem2a  12188  zsum  12191  fsum  12193  sumss  12197  sumss2  12199  fsumcvg2  12200  pcmpt  12940  pcmptdvds  12942  mbfpos  19006  mbfposb  19008  i1fposd  19062  isibl2  19121  nfitg  19129  cbvitg  19130  itgss3  19169  itgcn  19197  limcmpt  19233  rlimcnp2  20261  chirred  22975  nfprod1  24722  nfprod  24723  refsum2cn  27121  nfafv  27411  cdleme31sn  29942  cdleme32d  30006  cdleme32f  30008
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-if 3566
  Copyright terms: Public domain W3C validator