Theorem ifbid 3556

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 3555	. 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 1353   ifcif 3535

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 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-if 3536

This theorem is referenced by:  ifbieq1d  3557  ifbieq2d  3559  ifbieq12d  3561  ifandc  3573  ifordc  3574  nnnninf  7124  nnnninf2  7125  nnnninfeq  7126  nninfisollemne  7129  nninfisol  7131  fodjum  7144  fodju0  7145  fodjuomni  7147  fodjumkv  7158  nninfwlporlemd  7170  nninfwlpor  7172  nninfwlpoimlemg  7173  nninfwlpoimlemginf  7174  nninfwlpoim  7176  xaddval  9845  0tonninf  10439  1tonninf  10440  sumeq1  11363  summodc  11391  zsumdc  11392  fsum3  11395  isumss  11399  sumsplitdc  11440  prodeq1f  11560  zproddc  11587  fprodseq  11591  pcmpt  12341  pcmpt2  12342  pcfac  12348  lgsval  14408  lgsneg  14428  lgsdilem  14431  lgsdir2  14437  lgsdir  14439  bj-charfunbi  14566  subctctexmid  14753  nninfalllem1  14760  nninfsellemdc  14762  nninfself  14765  nninfsellemeq  14766  nninfsellemqall  14767  nninfsellemeqinf  14768  nninfomni  14771  nninffeq  14772  dceqnconst  14810  dcapnconst  14811