Theorem ifbid 3624

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 3623	. 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 105   = wceq 1395   ifcif 3602

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 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-if 3603

This theorem is referenced by:  ifbieq1d  3625  ifbieq2d  3627  ifbieq12d  3629  ifandc  3643  ifordc  3644  pw2f1odclem  6995  nnnninf  7293  nnnninf2  7294  nnnninfeq  7295  nninfisollemne  7298  nninfisol  7300  fodjum  7313  fodju0  7314  fodjuomni  7316  fodjumkv  7327  nninfwlporlemd  7339  nninfwlpor  7341  nninfwlpoimlemg  7342  nninfwlpoimlemginf  7343  nninfwlpoim  7346  nninfinfwlpo  7347  xaddval  10041  0tonninf  10662  1tonninf  10663  nninfinf  10665  sumeq1  11866  summodc  11894  zsumdc  11895  fsum3  11898  isumss  11902  sumsplitdc  11943  prodeq1f  12063  zproddc  12090  fprodseq  12094  nninfctlemfo  12561  pcmpt  12866  pcmpt2  12867  pcfac  12873  lgsval  15683  lgsneg  15703  lgsdilem  15706  lgsdir2  15712  lgsdir  15714  bj-charfunbi  16174  2omap  16359  pw1map  16361  subctctexmid  16366  nninfalllem1  16374  nninfsellemdc  16376  nninfself  16379  nninfsellemeq  16380  nninfsellemqall  16381  nninfsellemeqinf  16382  nninfomni  16385  nninffeq  16386  nnnninfex  16388  dceqnconst  16428  dcapnconst  16429