Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  nfif GIF version

Theorem nfif 3506
 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 9 . . 3 (⊤ → Ⅎ𝑥𝜑)
3 nfif.2 . . . 4 𝑥𝐴
43a1i 9 . . 3 (⊤ → 𝑥𝐴)
5 nfif.3 . . . 4 𝑥𝐵
65a1i 9 . . 3 (⊤ → 𝑥𝐵)
72, 4, 6nfifd 3505 . 2 (⊤ → 𝑥if(𝜑, 𝐴, 𝐵))
87mptru 1341 1 𝑥if(𝜑, 𝐴, 𝐵)
 Colors of variables: wff set class Syntax hints:  ⊤wtru 1333  Ⅎwnf 1437  Ⅎwnfc 2269  ifcif 3480 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122 This theorem depends on definitions:  df-bi 116  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-if 3481 This theorem is referenced by:  nfsum1  11177  nfsum  11178  sumrbdclem  11198  summodclem2a  11202  zsumdc  11205  fsum3  11208  isumss  11212  isumss2  11214  fsum3cvg2  11215  nfcprod1  11375  nfcprod  11376  cbvprod  11379  prodrbdclem  11392  prodmodclem2a  11397  zproddc  11400  fprodseq  11404
 Copyright terms: Public domain W3C validator