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

Theorem nfif 4089
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 4088 . 2 (⊤ → 𝑥if(𝜑, 𝐴, 𝐵))
87trud 1490 1 𝑥if(𝜑, 𝐴, 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wtru 1481  wnf 1705  wnfc 2748  ifcif 4060
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-if 4061
This theorem is referenced by:  csbif  4112  nfop  4388  nfrdg  7458  boxcutc  7898  nfoi  8366  nfsum1  14357  nfsum  14358  summolem2a  14382  zsum  14385  sumss  14391  sumss2  14393  fsumcvg2  14394  nfcprod  14569  cbvprod  14573  prodmolem2a  14592  zprod  14595  fprod  14599  fprodntriv  14600  prodss  14605  pcmpt  15523  pcmptdvds  15525  gsummpt1n0  18288  madugsum  20371  mbfpos  23331  mbfposb  23333  i1fposd  23387  isibl2  23446  nfitg  23454  cbvitg  23455  itgss3  23494  itgcn  23522  limcmpt  23560  rlimcnp2  24600  chirred  29115  cdleme31sn  35169  cdleme32d  35233  cdleme32f  35235  refsum2cn  38701  ssfiunibd  39005  uzub  39140  limsupubuz  39367  icccncfext  39421  fourierdlem86  39732  vonicc  40222  nfafv  40536
  Copyright terms: Public domain W3C validator