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

Theorem nfif 3505
 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

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 3504 . 2
87mptru 1341 1
 Colors of variables: wff set class Syntax hints:   wtru 1333  wnf 1437  wnfc 2269  cif 3479 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 3480 This theorem is referenced by:  nfsum1  11158  nfsum  11159  sumrbdclem  11179  summodclem2a  11183  zsumdc  11186  fsum3  11189  isumss  11193  isumss2  11195  fsum3cvg2  11196  nfcprod1  11356  nfcprod  11357  cbvprod  11360  prodrbdclem  11373  prodmodclem2a  11378  zproddc  11381  fprodseq  11385
 Copyright terms: Public domain W3C validator