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

Theorem ifbieq12d 4062
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 4057 . 2 (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐴, 𝐵))
3 ifbieq12d.2 . . 3 (𝜑𝐴 = 𝐶)
4 ifbieq12d.3 . . 3 (𝜑𝐵 = 𝐷)
53, 4ifeq12d 4055 . 2 (𝜑 → if(𝜒, 𝐴, 𝐵) = if(𝜒, 𝐶, 𝐷))
62, 5eqtrd 2643 1 (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐶, 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194   = wceq 1474  ifcif 4035
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rab 2904  df-v 3174  df-un 3544  df-if 4036
This theorem is referenced by:  csbif  4087  csbopg  4352  tz7.44-2  7367  tz7.44-3  7368  boxcutc  7814  unxpdomlem1  8026  dfac12lem1  8825  dfac12r  8828  fin23lem12  9013  fin23lem33  9027  ttukeylem3  9193  ttukey2g  9198  xaddval  11887  seqf1olem2  12658  expval  12679  ccatfval  13157  ccatval1  13160  ccatval2  13161  ccatalpha  13174  relexpsucnnr  13559  ruclem1  14745  eucalgval2  15078  ressval  15700  gsumvalx  17039  gsumpropd  17041  gsumpropd2lem  17042  gsumress  17045  mulgval  17312  pmtrfv  17641  mvrfval  19187  xrsdsval  19555  marrepeval  20130  marepveval  20135  mdetunilem9  20187  madutpos  20209  madugsum  20210  minmar1eval  20216  symgmatr01lem  20220  symgmatr01  20221  gsummatr01lem3  20224  gsummatr01lem4  20225  gsummatr01  20226  ptcmplem3  21610  xrhmeo  22484  phtpycc  22529  pcovalg  22551  pcocn  22556  pcohtpylem  22558  pcoass  22563  pcorevlem  22565  ovolunlem1a  22988  ovolunlem1  22989  ioombl1  23054  mbfmax  23139  mbfpos  23141  mbfi1fseqlem2  23206  mbfi1fseq  23211  ditgeq1  23335  ditgeq2  23336  ig1pval  23653  cxpval  24127  lgamgulmlem4  24475  lgamgulmlem5  24476  musumsum  24635  muinv  24636  lgsval  24743  gausslemma2dlem1a  24807  gausslemma2dlem2  24809  gausslemma2dlem3  24810  gausslemma2dlem4  24811  clwlkisclwwlklem2fv1  26076  resvval  28964  psgnfzto1stlem  28987  smatrcl  28996  smatlem  28997  madjusmdetlem2  29028  madjusmdet  29031  ballotlemsv  29704  ballotlemsf1o  29708  plymulx0  29756  mrsubcv  30467  mrsubrn  30470  rdgprc0  30749  dfrdg2  30751  csbrdgg  32147  csbfinxpg  32197  finxpreclem3  32202  poimirlem2  32377  poimirlem23  32398  poimirlem24  32399  poimirlem27  32402  itg2addnclem3  32429  itgaddnclem2  32435  ftc1anclem5  32455  cdleme27b  34470  cdleme29b  34477  cdleme31sn  34482  cdleme31fv  34492  cdleme40v  34571  dihffval  35333  dihfval  35334  dihval  35335  aomclem8  36445  ifeq123d  38027  icccncfext  38570  dvnxpaek  38629  ioorrnopn  38998  ioorrnopnxr  39000  hsphoival  39266  sge0hsphoire  39276  hoidmvlelem1  39282  hoidmvlelem2  39283  hoidmvlelem3  39284  hoidmvlelem4  39285  hoidmvlelem5  39286  hoidifhspval3  39306  hspmbllem2  39314  ovolval4  39338  vtxval  40228  iedgval  40229  crctcsh1wlkn0lem2  41009  crctcsh1wlkn0lem3  41010  crctcshlem4  41018  crctcsh  41022  clwlkclwwlklem2fv1  41199  eucrct2eupth  41408
  Copyright terms: Public domain W3C validator