Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ifbieq12d Structured version   Visualization version   GIF version

Theorem ifbieq12d 4146
 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
StepHypRef Expression
1 ifbieq12d.1 . . 3 (𝜑 → (𝜓𝜒))
21ifbid 4141 . 2 (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐴, 𝐵))
3 ifbieq12d.2 . . 3 (𝜑𝐴 = 𝐶)
4 ifbieq12d.3 . . 3 (𝜑𝐵 = 𝐷)
53, 4ifeq12d 4139 . 2 (𝜑 → if(𝜒, 𝐴, 𝐵) = if(𝜒, 𝐶, 𝐷))
62, 5eqtrd 2685 1 (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐶, 𝐷))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   = wceq 1523  ifcif 4119 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-un 3612  df-if 4120 This theorem is referenced by:  csbif  4171  csbopg  4451  tz7.44-2  7548  tz7.44-3  7549  boxcutc  7993  unxpdomlem1  8205  dfac12lem1  9003  dfac12r  9006  fin23lem12  9191  fin23lem33  9205  ttukeylem3  9371  ttukey2g  9376  xaddval  12092  seqf1olem2  12881  expval  12902  ccatfval  13391  ccatval1  13395  ccatval2  13396  ccatalpha  13411  relexpsucnnr  13809  ruclem1  15004  eucalgval2  15341  setsstruct  15945  ressval  15974  gsumvalx  17317  gsumpropd  17319  gsumpropd2lem  17320  gsumress  17323  mulgval  17590  pmtrfv  17918  mvrfval  19468  xrsdsval  19838  marrepeval  20417  marepveval  20422  mdetunilem9  20474  madutpos  20496  madugsum  20497  minmar1eval  20503  symgmatr01lem  20507  symgmatr01  20508  gsummatr01lem3  20511  gsummatr01lem4  20512  gsummatr01  20513  ptcmplem3  21905  xrhmeo  22792  phtpycc  22837  pcovalg  22858  pcocn  22863  pcohtpylem  22865  pcoass  22870  pcorevlem  22872  ovolunlem1a  23310  ovolunlem1  23311  ioombl1  23376  mbfmax  23461  mbfpos  23463  mbfi1fseqlem2  23528  mbfi1fseq  23533  ditgeq1  23657  ditgeq2  23658  ig1pval  23977  cxpval  24455  lgamgulmlem4  24803  lgamgulmlem5  24804  musumsum  24963  muinv  24964  lgsval  25071  gausslemma2dlem1a  25135  gausslemma2dlem2  25137  gausslemma2dlem3  25138  gausslemma2dlem4  25139  vtxval  25923  iedgval  25924  vtxvalOLD  25925  iedgvalOLD  25926  crctcshwlkn0lem2  26759  crctcshwlkn0lem3  26760  crctcshlem4  26768  crctcsh  26772  clwlkclwwlklem2fv1  26961  eucrct2eupth  27223  resvval  29955  psgnfzto1stlem  29978  smatrcl  29990  smatlem  29991  madjusmdetlem2  30022  madjusmdet  30025  ballotlemsv  30699  ballotlemsf1o  30703  plymulx0  30752  mrsubcv  31533  mrsubrn  31536  rdgprc0  31823  dfrdg2  31825  csbrdgg  33305  csbfinxpg  33355  finxpreclem3  33360  poimirlem2  33541  poimirlem23  33562  poimirlem24  33563  poimirlem27  33566  itg2addnclem3  33593  itgaddnclem2  33599  ftc1anclem5  33619  cdleme27b  35973  cdleme29b  35980  cdleme31sn  35985  cdleme31fv  35995  cdleme40v  36074  dihffval  36836  dihfval  36837  dihval  36838  aomclem8  37948  ifeq123d  39521  icccncfext  40418  dvnxpaek  40475  ioorrnopn  40843  ioorrnopnxr  40845  hsphoival  41114  sge0hsphoire  41124  hoidmvlelem1  41130  hoidmvlelem2  41131  hoidmvlelem3  41132  hoidmvlelem4  41133  hoidmvlelem5  41134  hoidifhspval3  41154  hspmbllem2  41162  ovolval4  41186
 Copyright terms: Public domain W3C validator