Theorem ifbieq12d 4557

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 4552	. 2 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐴, 𝐵))
3		ifbieq12d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐶)
4		ifbieq12d.3	. . 3 ⊢ (𝜑 → 𝐵 = 𝐷)
5	3, 4	ifeq12d 4550	. 2 ⊢ (𝜑 → if(𝜒, 𝐴, 𝐵) = if(𝜒, 𝐶, 𝐷))
6	2, 5	eqtrd 2768	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐶, 𝐷))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1534  ifcif 4529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-rab 3430  df-v 3473  df-un 3952  df-if 4530

This theorem is referenced by:  csbif  4586  csbopg  4892  tz7.44-2  8428  tz7.44-3  8429  boxcutc  8960  unxpdomlem1  9275  ttrcltr  9740  updjudhcoinlf  9956  updjudhcoinrg  9957  dfac12lem1  10167  dfac12r  10170  fin23lem12  10355  fin23lem33  10369  ttukeylem3  10535  ttukey2g  10540  xaddval  13235  seqf1olem2  14040  expval  14061  ccatfval  14556  ccatval1  14560  ccatval2  14561  ccatalpha  14576  relexpsucnnr  15005  ruclem1  16208  eucalgval2  16552  setsstruct  17145  ressval  17212  gsumvalx  18636  gsumpropd  18638  gsumpropd2lem  18639  gsumress  18642  mulgval  19027  pmtrfv  19407  xrsdsval  21343  mvrfval  21923  selvfval  22060  marrepeval  22478  marepveval  22483  mdetunilem9  22535  madutpos  22557  madugsum  22558  minmar1eval  22564  symgmatr01lem  22568  symgmatr01  22569  gsummatr01lem3  22572  gsummatr01lem4  22573  gsummatr01  22574  ptcmplem3  23971  xrhmeo  24884  phtpycc  24930  pcovalg  24952  pcocn  24957  pcohtpylem  24959  pcoass  24964  pcorevlem  24966  ovolunlem1a  25438  ovolunlem1  25439  ioombl1  25504  mbfmax  25591  mbfpos  25593  mbfi1fseqlem2  25659  mbfi1fseq  25664  ditgeq1  25790  ditgeq2  25791  ig1pval  26123  cxpval  26611  lgamgulmlem4  26977  lgamgulmlem5  26978  musumsum  27137  muinv  27138  lgsval  27247  gausslemma2dlem1a  27311  gausslemma2dlem2  27313  gausslemma2dlem3  27314  gausslemma2dlem4  27315  abssval  28146  vtxval  28826  iedgval  28827  crctcshwlkn0lem2  29635  crctcshwlkn0lem3  29636  crctcshlem4  29644  crctcsh  29648  clwlkclwwlklem2fv1  29818  eucrct2eupth  30068  psgnfzto1stlem  32834  resvval  33051  smatrcl  33397  smatlem  33398  madjusmdetlem2  33429  madjusmdet  33432  ballotlemsv  34129  ballotlemsf1o  34133  plymulx0  34179  mrsubcv  35120  mrsubrn  35123  rdgprc0  35389  dfrdg2  35391  csbrdgg  36808  csbfinxpg  36867  finxpreclem3  36872  poimirlem2  37095  poimirlem23  37116  poimirlem24  37117  poimirlem27  37120  itg2addnclem3  37146  itgaddnclem2  37152  ftc1anclem5  37170  cdleme27b  39841  cdleme29b  39848  cdleme31sn  39853  cdleme31fv  39863  cdleme40v  39942  dihffval  40703  dihfval  40704  dihval  40705  metakunt3  41659  metakunt4  41660  metakunt6  41662  metakunt7  41663  metakunt8  41664  metakunt10  41666  metakunt11  41667  metakunt12  41668  metakunt20  41676  metakunt21  41677  metakunt22  41678  metakunt32  41688  selvvvval  41818  prjspnfv01  42048  prjspner01  42049  prjspner1  42050  aomclem8  42485  mnringvald  43645  icccncfext  45275  dvnxpaek  45330  fourierdlem103  45597  fourierdlem104  45598  ioorrnopn  45693  ioorrnopnxr  45695  hsphoival  45967  sge0hsphoire  45977  hoidmvlelem1  45983  hoidmvlelem2  45984  hoidmvlelem3  45985  hoidmvlelem4  45986  hoidmvlelem5  45987  hoidifhspval3  46007  hspmbllem2  46015  ovolval4  46039  afv2eq12d  46595

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »