Theorem ifbid 3548

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

Step	Hyp	Ref	Expression
1		ifbid.1	. 2 |- ( ph -> ( ps <-> ch ) )
2		ifbi 3547	. 2 |- ( ( ps <-> ch ) -> if ( ps , A , B ) = if ( ch , A , B ) )
3	1, 2	syl 14	1 |- ( ph -> if ( ps , A , B ) = if ( ch , A , B ) )

Syntax hints:   -> wi 4   <-> wb 104   = wceq 1349   ifcif 3527

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 610  ax-in2 611  ax-io 705  ax-5 1441  ax-7 1442  ax-gen 1443  ax-ie1 1487  ax-ie2 1488  ax-8 1498  ax-11 1500  ax-4 1504  ax-17 1520  ax-i9 1524  ax-ial 1528  ax-i5r 1529  ax-ext 2153

This theorem depends on definitions:  df-bi 116  df-tru 1352  df-nf 1455  df-sb 1757  df-clab 2158  df-cleq 2164  df-if 3528

This theorem is referenced by:  ifbieq1d  3549  ifbieq2d  3551  ifbieq12d  3553  ifandc  3564  ifordc  3565  nnnninf  7106  nnnninf2  7107  nnnninfeq  7108  nninfisollemne  7111  nninfisol  7113  fodjum  7126  fodju0  7127  fodjuomni  7129  fodjumkv  7140  nninfwlporlemd  7152  nninfwlpor  7154  nninfwlpoimlemg  7155  nninfwlpoimlemginf  7156  nninfwlpoim  7158  xaddval  9806  0tonninf  10399  1tonninf  10400  sumeq1  11322  summodc  11350  zsumdc  11351  fsum3  11354  isumss  11358  sumsplitdc  11399  prodeq1f  11519  zproddc  11546  fprodseq  11550  pcmpt  12299  pcmpt2  12300  pcfac  12306  lgsval  13784  lgsneg  13804  lgsdilem  13807  lgsdir2  13813  lgsdir  13815  bj-charfunbi  13931  subctctexmid  14119  nninfalllem1  14126  nninfsellemdc  14128  nninfself  14131  nninfsellemeq  14132  nninfsellemqall  14133  nninfsellemeqinf  14134  nninfomni  14137  nninffeq  14138  dceqnconst  14176  dcapnconst  14177