Theorem ifbieq2d 3525

Description: Equivalence/equality deduction for conditional operators. (Contributed by Paul Chapman, 22-Jun-2011.)

Hypotheses

Ref	Expression
ifbieq2d.1	|- ( ph -> ( ps <-> ch ) )
ifbieq2d.2	|- ( ph -> A = B )

Assertion

Ref	Expression
ifbieq2d	|- ( ph -> if ( ps , C , A ) = if ( ch , C , B ) )

Proof of Theorem ifbieq2d

Step	Hyp	Ref	Expression
1		ifbieq2d.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	ifbid 3522	. 2 |- ( ph -> if ( ps , C , A ) = if ( ch , C , A ) )
3		ifbieq2d.2	. . 3 |- ( ph -> A = B )
4	3	ifeq2d 3519	. 2 |- ( ph -> if ( ch , C , A ) = if ( ch , C , B ) )
5	2, 4	eqtrd 2187	1 |- ( ph -> if ( ps , C , A ) = if ( ch , C , B ) )

Syntax hints:   -> wi 4   <-> wb 104   = wceq 1332   ifcif 3501

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 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1481  ax-10 1482  ax-11 1483  ax-i12 1484  ax-bndl 1486  ax-4 1487  ax-17 1503  ax-i9 1507  ax-ial 1511  ax-i5r 1512  ax-ext 2136

This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1740  df-clab 2141  df-cleq 2147  df-clel 2150  df-nfc 2285  df-rab 2441  df-v 2711  df-un 3102  df-if 3502

This theorem is referenced by:  difinfsnlem  7029  ctmlemr  7038  xnegeq  9709  xaddval  9727  iseqf1olemqval  10364  iseqf1olemqk  10371  seq3f1olemqsum  10377  exp3val  10399  gcdval  11815  gcdass  11870  lcmval  11911  lcmass  11933  ennnfonelemj0  12081  ennnfonelemjn  12082  ennnfonelem0  12085  ennnfonelemp1  12086  ennnfonelemnn0  12102  nnsf  13517  peano4nninf  13518  peano3nninf  13519  exmidsbthr  13535