Theorem ifbieq2d 4486

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

Hypotheses

Ref	Expression
ifbieq2d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
ifbieq2d.2	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
ifbieq2d	⊢ (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜒, 𝐶, 𝐵))

Proof of Theorem ifbieq2d

Step	Hyp	Ref	Expression
1		ifbieq2d.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	ifbid 4483	. 2 ⊢ (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜒, 𝐶, 𝐴))
3		ifbieq2d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
4	3	ifeq2d 4480	. 2 ⊢ (𝜑 → if(𝜒, 𝐶, 𝐴) = if(𝜒, 𝐶, 𝐵))
5	2, 4	eqtrd 2779	1 ⊢ (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜒, 𝐶, 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  ifcif 4460

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-un 3893  df-if 4461

This theorem is referenced by:  tz7.44-2  8247  tz7.44-3  8248  oev  8353  cantnfp1lem1  9445  cantnfp1lem3  9447  ttrclselem2  9493  fin23lem12  10096  fin23lem33  10110  axcc2  10202  ttukeylem3  10276  ttukey2g  10281  canthp1lem2  10418  canthp1  10419  xnegeq  12950  xaddval  12966  xmulval  12968  expval  13793  cshfn  14512  ofccat  14689  relexpsucnnr  14745  sgnval  14808  sadcp1  16171  smupp1  16196  gcdval  16212  gcdass  16264  lcmval  16306  lcmass  16328  lcmfval  16335  lcmf0val  16336  lcmfpr  16341  iserodd  16545  pcval  16554  vdwlem6  16696  ramub1lem2  16737  ramcl  16739  mulgval  18713  symgextfv  19035  symgfixfo  19056  odfval  19149  odval  19151  submod  19183  gexval  19192  znval  20748  fvmptnn04if  22007  cpmadumatpoly  22041  cayleyhamilton  22048  cayleyhamiltonALT  22049  ptcmplem2  23213  iccpnfhmeo  24117  pcopt  24194  ioombl1  24735  ioorval  24747  uniioombllem6  24761  itg1addlem3  24871  itg2uba  24917  limcfval  25045  limcmpt  25056  limcco  25066  dvcobr  25119  ig1pval  25346  abelthlem9  25608  logtayllem  25823  logtayl  25824  leibpilem2  26100  rlimcnp2  26125  efrlim  26128  igamval  26205  muval  26290  lgsval  26458  lgsfval  26459  lgsval2lem  26464  rpvmasum2  26669  padicval  26774  padicabv  26787  axlowdimlem15  27333  axlowdim  27338  eupth2lem3lem3  28603  eupth2  28612  eucrct2eupth  28618  psgnfzto1stlem  31376  sgnsv  31436  sgnsval  31437  madjusmdetlem2  31787  madjusmdet  31790  xrge0iifcv  31893  xrge0iifhom  31896  xrge0tmd  31904  xrge0tmdALT  31905  signspval  32540  ex-sategoelel  33392  rdgprc0  33778  dfrdg2  33780  dfrdg4  34262  csbrdgg  35509  finxpeq1  35566  finxpreclem3  35573  poimirlem1  35787  poimirlem7  35793  poimirlem10  35796  poimirlem11  35797  itg2addnclem  35837  itg2addnclem3  35839  itg2addnc  35840  fdc  35912  heiborlem4  35981  heiborlem6  35983  heiborlem10  35987  mapdhval  39745  hdmap1fval  39817  hdmap1vallem  39818  hdmap1val  39819  hdmap1cbv  39823  sticksstones10  40118  sticksstones12a  40120  metakunt3  40134  metakunt4  40135  metakunt6  40137  metakunt7  40138  metakunt8  40139  metakunt10  40141  metakunt11  40142  metakunt12  40143  metakunt20  40151  metakunt21  40152  metakunt22  40153  fsuppind  40286  irrapxlem4  40654  clsk1indlem0  41658  clsk1indlem2  41659  clsk1indlem3  41660  clsk1indlem4  41661  clsk1indlem1  41662  dirkerval2  43642  dirkeritg  43650  dirkercncf  43655  fourierdlem29  43684  fourierdlem37  43692  fourierdlem62  43716  fourierdlem79  43733  fourierdlem81  43735  fourierdlem82  43736  fourierdlem92  43746  fourierdlem96  43750  fourierdlem97  43751  fourierdlem98  43752  fourierdlem99  43753  fourierdlem105  43759  fourierdlem108  43762  fourierdlem110  43764  fourierdlem112  43766  fourierdlem113  43767  fouriersw  43779  etransclem24  43806  etransclem25  43807  etransclem31  43813  etransclem35  43817  etransclem37  43819  sge0val  43911  nnfoctbdjlem  44000  nnfoctbdj  44001  ovnval  44086  ovnval2  44090  ovnval2b  44097  hsphoif  44121  hoidmvval  44122  hsphoival  44124  hoidmv1lelem1  44136  hoidmv1lelem2  44137  hoidmv1lelem3  44138  hoidmv1le  44139  ovnhoi  44148  hoidifhspval  44153  hspmbllem2  44172  ovnsubadd2  44191  blenval  45928