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  7003  nnnninf  7304  nnnninf2  7305  nnnninfeq  7306  nninfisollemne  7309  nninfisol  7311  fodjum  7324  fodju0  7325  fodjuomni  7327  fodjumkv  7338  nninfwlporlemd  7350  nninfwlpor  7352  nninfwlpoimlemg  7353  nninfwlpoimlemginf  7354  nninfwlpoim  7357  nninfinfwlpo  7358  xaddval  10053  0tonninf  10674  1tonninf  10675  nninfinf  10677  sumeq1  11882  summodc  11910  zsumdc  11911  fsum3  11914  isumss  11918  sumsplitdc  11959  prodeq1f  12079  zproddc  12106  fprodseq  12110  nninfctlemfo  12577  pcmpt  12882  pcmpt2  12883  pcfac  12889  lgsval  15699  lgsneg  15719  lgsdilem  15722  lgsdir2  15728  lgsdir  15730  bj-charfunbi  16257  2omap  16446  pw1map  16448  subctctexmid  16453  nninfalllem1  16462  nninfsellemdc  16464  nninfself  16467  nninfsellemeq  16468  nninfsellemqall  16469  nninfsellemeqinf  16470  nninfomni  16473  nninffeq  16474  nnnninfex  16476  dceqnconst  16516  dcapnconst  16517