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

Theorem ifbid 3537
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 3536 . 2 ((𝜓𝜒) → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐴, 𝐵))
31, 2syl 14 1 (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐴, 𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104   = wceq 1342  ifcif 3516
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 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-11 1493  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-ext 2146
This theorem depends on definitions:  df-bi 116  df-tru 1345  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-if 3517
This theorem is referenced by:  ifbieq1d  3538  ifbieq2d  3540  ifbieq12d  3542  ifandc  3552  nnnninf  7082  nnnninf2  7083  nnnninfeq  7084  nninfisollemne  7087  nninfisol  7089  fodjum  7102  fodju0  7103  fodjuomni  7105  fodjumkv  7116  xaddval  9773  0tonninf  10365  1tonninf  10366  sumeq1  11286  summodc  11314  zsumdc  11315  fsum3  11318  isumss  11322  sumsplitdc  11363  prodeq1f  11483  zproddc  11510  fprodseq  11514  pcmpt  12262  pcmpt2  12263  pcfac  12269  bj-charfunbi  13555  subctctexmid  13743  nninfalllem1  13750  nninfsellemdc  13752  nninfself  13755  nninfsellemeq  13756  nninfsellemqall  13757  nninfsellemeqinf  13758  nninfomni  13761  nninffeq  13762  dceqnconst  13800  dcapnconst  13801
  Copyright terms: Public domain W3C validator