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

Theorem ifbid 3570
Description: Equivalence deduction for conditional operators. (Contributed by NM, 18-Apr-2005.)
Hypothesis
Ref Expression
ifbid.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
ifbid (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐴, 𝐵))

Proof of Theorem ifbid
StepHypRef Expression
1 ifbid.1 . 2 (𝜑 → (𝜓𝜒))
2 ifbi 3569 . 2 ((𝜓𝜒) → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐴, 𝐵))
31, 2syl 14 1 (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐴, 𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 105   = wceq 1364  ifcif 3549
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171
This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-if 3550
This theorem is referenced by:  ifbieq1d  3571  ifbieq2d  3573  ifbieq12d  3575  ifandc  3587  ifordc  3588  pw2f1odclem  6857  nnnninf  7149  nnnninf2  7150  nnnninfeq  7151  nninfisollemne  7154  nninfisol  7156  fodjum  7169  fodju0  7170  fodjuomni  7172  fodjumkv  7183  nninfwlporlemd  7195  nninfwlpor  7197  nninfwlpoimlemg  7198  nninfwlpoimlemginf  7199  nninfwlpoim  7201  xaddval  9870  0tonninf  10465  1tonninf  10466  sumeq1  11390  summodc  11418  zsumdc  11419  fsum3  11422  isumss  11426  sumsplitdc  11467  prodeq1f  11587  zproddc  11614  fprodseq  11618  pcmpt  12370  pcmpt2  12371  pcfac  12377  lgsval  14842  lgsneg  14862  lgsdilem  14865  lgsdir2  14871  lgsdir  14873  bj-charfunbi  15000  subctctexmid  15188  nninfalllem1  15195  nninfsellemdc  15197  nninfself  15200  nninfsellemeq  15201  nninfsellemqall  15202  nninfsellemeqinf  15203  nninfomni  15206  nninffeq  15207  dceqnconst  15246  dcapnconst  15247
  Copyright terms: Public domain W3C validator