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

Theorem nfif 4065
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 4064 . 2 (⊤ → 𝑥if(𝜑, 𝐴, 𝐵))
87trud 1484 1 𝑥if(𝜑, 𝐴, 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wtru 1476  wnf 1699  wnfc 2738  ifcif 4036
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-if 4037
This theorem is referenced by:  csbif  4088  nfop  4356  nfrdg  7397  boxcutc  7837  nfoi  8302  nfsum1  14268  nfsum  14269  summolem2a  14293  zsum  14296  sumss  14302  sumss2  14304  fsumcvg2  14305  nfcprod  14480  cbvprod  14484  prodmolem2a  14503  zprod  14506  fprod  14510  fprodntriv  14511  prodss  14516  pcmpt  15434  pcmptdvds  15436  gsummpt1n0  18187  madugsum  20268  mbfpos  23224  mbfposb  23226  i1fposd  23280  isibl2  23339  nfitg  23347  cbvitg  23348  itgss3  23387  itgcn  23415  limcmpt  23453  rlimcnp2  24493  chirred  28638  cdleme31sn  34686  cdleme32d  34750  cdleme32f  34752  refsum2cn  38220  ssfiunibd  38464  icccncfext  38773  fourierdlem86  39085  vonicc  39576  nfafv  39865
  Copyright terms: Public domain W3C validator