Theorem ifbid 3546

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 3545	. 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 1348   ifcif 3525

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 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-if 3526

This theorem is referenced by:  ifbieq1d  3547  ifbieq2d  3549  ifbieq12d  3551  ifandc  3562  nnnninf  7098  nnnninf2  7099  nnnninfeq  7100  nninfisollemne  7103  nninfisol  7105  fodjum  7118  fodju0  7119  fodjuomni  7121  fodjumkv  7132  xaddval  9789  0tonninf  10382  1tonninf  10383  sumeq1  11305  summodc  11333  zsumdc  11334  fsum3  11337  isumss  11341  sumsplitdc  11382  prodeq1f  11502  zproddc  11529  fprodseq  11533  pcmpt  12282  pcmpt2  12283  pcfac  12289  lgsval  13620  lgsneg  13640  lgsdilem  13643  lgsdir2  13649  lgsdir  13651  bj-charfunbi  13768  subctctexmid  13956  nninfalllem1  13963  nninfsellemdc  13965  nninfself  13968  nninfsellemeq  13969  nninfsellemqall  13970  nninfsellemeqinf  13971  nninfomni  13974  nninffeq  13975  dceqnconst  14013  dcapnconst  14014