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

Theorem nfif 4515
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 𝑥𝜑
nfif.2 𝑥𝐴
nfif.3 𝑥𝐵
Assertion
Ref Expression
nfif 𝑥if(𝜑, 𝐴, 𝐵)

Proof of Theorem nfif
StepHypRef Expression
1 nfif.1 . . . 4 𝑥𝜑
21a1i 11 . . 3 (⊤ → Ⅎ𝑥𝜑)
3 nfif.2 . . . 4 𝑥𝐴
43a1i 11 . . 3 (⊤ → 𝑥𝐴)
5 nfif.3 . . . 4 𝑥𝐵
65a1i 11 . . 3 (⊤ → 𝑥𝐵)
72, 4, 6nfifd 4514 . 2 (⊤ → 𝑥if(𝜑, 𝐴, 𝐵))
87mptru 1548 1 𝑥if(𝜑, 𝐴, 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wtru 1542  wnf 1785  wnfc 2886  ifcif 4485
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2888  df-if 4486
This theorem is referenced by:  csbif  4542  nfop  4845  nfrdg  8357  boxcutc  8876  nfoi  9447  nfsum1  15571  nfsum  15572  nfsumOLD  15573  summolem2a  15597  zsum  15600  sumss  15606  sumss2  15608  fsumcvg2  15609  nfcprod  15791  cbvprod  15795  prodmolem2a  15814  zprod  15817  fprod  15821  fprodntriv  15822  prodss  15827  pcmpt  16761  pcmptdvds  16763  gsummpt1n0  19738  madugsum  21988  mbfpos  25011  mbfposb  25013  i1fposd  25068  isibl2  25127  nfitg  25135  cbvitg  25136  itgss3  25175  itgcn  25205  limcmpt  25243  rlimcnp2  26312  nosupbnd2  27060  noinfbnd2  27075  chirred  31235  cdleme31sn  38832  cdleme32d  38896  cdleme32f  38898  refsum2cn  43223  ssfiunibd  43517  uzub  43640  limsupubuz  43924  icccncfext  44098  fourierdlem86  44403  vonicc  44896  nfafv  45338  nfafv2  45420
  Copyright terms: Public domain W3C validator