Theorem ifbieq12d 4494

Description: Equivalence deduction for conditional operators. (Contributed by Jeff Madsen, 2-Sep-2009.)

Hypotheses

Ref	Expression
ifbieq12d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
ifbieq12d.2	⊢ (𝜑 → 𝐴 = 𝐶)
ifbieq12d.3	⊢ (𝜑 → 𝐵 = 𝐷)

Assertion

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

Proof of Theorem ifbieq12d

Step	Hyp	Ref	Expression
1		ifbieq12d.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	ifbid 4489	. 2 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐴, 𝐵))
3		ifbieq12d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐶)
4		ifbieq12d.3	. . 3 ⊢ (𝜑 → 𝐵 = 𝐷)
5	3, 4	ifeq12d 4487	. 2 ⊢ (𝜑 → if(𝜒, 𝐴, 𝐵) = if(𝜒, 𝐶, 𝐷))
6	2, 5	eqtrd 2856	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐶, 𝐷))

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1537  ifcif 4467

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-un 3941  df-if 4468

This theorem is referenced by:  csbif  4522  csbopg  4821  tz7.44-2  8043  tz7.44-3  8044  boxcutc  8505  unxpdomlem1  8722  updjudhcoinlf  9361  updjudhcoinrg  9362  dfac12lem1  9569  dfac12r  9572  fin23lem12  9753  fin23lem33  9767  ttukeylem3  9933  ttukey2g  9938  xaddval  12617  seqf1olem2  13411  expval  13432  ccatfval  13925  ccatval1  13930  ccatval1OLD  13931  ccatval2  13932  ccatalpha  13947  relexpsucnnr  14384  ruclem1  15584  eucalgval2  15925  setsstruct  16523  ressval  16551  gsumvalx  17886  gsumpropd  17888  gsumpropd2lem  17889  gsumress  17892  mulgval  18228  pmtrfv  18580  mvrfval  20200  selvfval  20330  xrsdsval  20589  marrepeval  21172  marepveval  21177  mdetunilem9  21229  madutpos  21251  madugsum  21252  minmar1eval  21258  symgmatr01lem  21262  symgmatr01  21263  gsummatr01lem3  21266  gsummatr01lem4  21267  gsummatr01  21268  ptcmplem3  22662  xrhmeo  23550  phtpycc  23595  pcovalg  23616  pcocn  23621  pcohtpylem  23623  pcoass  23628  pcorevlem  23630  ovolunlem1a  24097  ovolunlem1  24098  ioombl1  24163  mbfmax  24250  mbfpos  24252  mbfi1fseqlem2  24317  mbfi1fseq  24322  ditgeq1  24446  ditgeq2  24447  ig1pval  24766  cxpval  25247  lgamgulmlem4  25609  lgamgulmlem5  25610  musumsum  25769  muinv  25770  lgsval  25877  gausslemma2dlem1a  25941  gausslemma2dlem2  25943  gausslemma2dlem3  25944  gausslemma2dlem4  25945  vtxval  26785  iedgval  26786  crctcshwlkn0lem2  27589  crctcshwlkn0lem3  27590  crctcshlem4  27598  crctcsh  27602  clwlkclwwlklem2fv1  27773  eucrct2eupth  28024  psgnfzto1stlem  30742  resvval  30900  smatrcl  31061  smatlem  31062  madjusmdetlem2  31093  madjusmdet  31096  ballotlemsv  31767  ballotlemsf1o  31771  plymulx0  31817  mrsubcv  32757  mrsubrn  32760  rdgprc0  33038  dfrdg2  33040  csbrdgg  34613  csbfinxpg  34672  finxpreclem3  34677  poimirlem2  34909  poimirlem23  34930  poimirlem24  34931  poimirlem27  34934  itg2addnclem3  34960  itgaddnclem2  34966  ftc1anclem5  34986  cdleme27b  37519  cdleme29b  37526  cdleme31sn  37531  cdleme31fv  37541  cdleme40v  37620  dihffval  38381  dihfval  38382  dihval  38383  aomclem8  39681  icccncfext  42190  dvnxpaek  42247  fourierdlem103  42514  fourierdlem104  42515  ioorrnopn  42610  ioorrnopnxr  42612  hsphoival  42881  sge0hsphoire  42891  hoidmvlelem1  42897  hoidmvlelem2  42898  hoidmvlelem3  42899  hoidmvlelem4  42900  hoidmvlelem5  42901  hoidifhspval3  42921  hspmbllem2  42929  ovolval4  42953  afv2eq12d  43434