Theorem ifbid 3592

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 3591	. 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 1373   ifcif 3571

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 615  ax-in2 616  ax-io 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-if 3572

This theorem is referenced by:  ifbieq1d  3593  ifbieq2d  3595  ifbieq12d  3597  ifandc  3610  ifordc  3611  pw2f1odclem  6933  nnnninf  7230  nnnninf2  7231  nnnninfeq  7232  nninfisollemne  7235  nninfisol  7237  fodjum  7250  fodju0  7251  fodjuomni  7253  fodjumkv  7264  nninfwlporlemd  7276  nninfwlpor  7278  nninfwlpoimlemg  7279  nninfwlpoimlemginf  7280  nninfwlpoim  7283  nninfinfwlpo  7284  xaddval  9969  0tonninf  10587  1tonninf  10588  nninfinf  10590  sumeq1  11699  summodc  11727  zsumdc  11728  fsum3  11731  isumss  11735  sumsplitdc  11776  prodeq1f  11896  zproddc  11923  fprodseq  11927  nninfctlemfo  12394  pcmpt  12699  pcmpt2  12700  pcfac  12706  lgsval  15514  lgsneg  15534  lgsdilem  15537  lgsdir2  15543  lgsdir  15545  bj-charfunbi  15784  2omap  15969  subctctexmid  15974  nninfalllem1  15982  nninfsellemdc  15984  nninfself  15987  nninfsellemeq  15988  nninfsellemqall  15989  nninfsellemeqinf  15990  nninfomni  15993  nninffeq  15994  nnnninfex  15996  dceqnconst  16036  dcapnconst  16037