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

Theorem ifbid 3463
Description: Equivalence deduction for conditional operators. (Contributed by NM, 18-Apr-2005.)
Hypothesis
Ref Expression
ifbid.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
ifbid  |-  ( ph  ->  if ( ps ,  A ,  B )  =  if ( ch ,  A ,  B )
)

Proof of Theorem ifbid
StepHypRef Expression
1 ifbid.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
2 ifbi 3462 . 2  |-  ( ( ps  <->  ch )  ->  if ( ps ,  A ,  B )  =  if ( ch ,  A ,  B ) )
31, 2syl 14 1  |-  ( ph  ->  if ( ps ,  A ,  B )  =  if ( ch ,  A ,  B )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104    = wceq 1316   ifcif 3444
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 588  ax-in2 589  ax-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-11 1469  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-if 3445
This theorem is referenced by:  ifbieq1d  3464  ifbieq2d  3466  ifbieq12d  3468  ifandc  3478  fodjum  6986  fodju0  6987  fodjuomni  6989  nnnninf  6991  fodjumkv  7002  xaddval  9583  0tonninf  10167  1tonninf  10168  sumeq1  11079  summodc  11107  zsumdc  11108  fsum3  11111  isumss  11115  sumsplitdc  11156  subctctexmid  13092  nninfalllemn  13098  nninfalllem1  13099  nninfsellemdc  13102  nninfself  13105  nninfsellemeq  13106  nninfsellemqall  13107  nninfsellemeqinf  13108  nninfomni  13111  nninffeq  13112
  Copyright terms: Public domain W3C validator