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

Theorem ifbieq12d 4455
 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 4450 . 2 (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐴, 𝐵))
3 ifbieq12d.2 . . 3 (𝜑𝐴 = 𝐶)
4 ifbieq12d.3 . . 3 (𝜑𝐵 = 𝐷)
53, 4ifeq12d 4448 . 2 (𝜑 → if(𝜒, 𝐴, 𝐵) = if(𝜒, 𝐶, 𝐷))
62, 5eqtrd 2836 1 (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐶, 𝐷))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538  ifcif 4428 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-12 2176  ax-ext 2773 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-rab 3118  df-v 3446  df-un 3889  df-if 4429 This theorem is referenced by:  csbif  4483  csbopg  4786  tz7.44-2  8030  tz7.44-3  8031  boxcutc  8492  unxpdomlem1  8710  updjudhcoinlf  9349  updjudhcoinrg  9350  dfac12lem1  9558  dfac12r  9561  fin23lem12  9746  fin23lem33  9760  ttukeylem3  9926  ttukey2g  9931  xaddval  12608  seqf1olem2  13410  expval  13431  ccatfval  13920  ccatval1  13925  ccatval1OLD  13926  ccatval2  13927  ccatalpha  13942  relexpsucnnr  14380  ruclem1  15580  eucalgval2  15919  setsstruct  16519  ressval  16547  gsumvalx  17882  gsumpropd  17884  gsumpropd2lem  17885  gsumress  17888  mulgval  18224  pmtrfv  18576  xrsdsval  20139  mvrfval  20662  selvfval  20793  marrepeval  21172  marepveval  21177  mdetunilem9  21229  madutpos  21251  madugsum  21252  minmar1eval  21258  symgmatr01lem  21262  symgmatr01  21263  gsummatr01lem3  21266  gsummatr01lem4  21267  gsummatr01  21268  ptcmplem3  22663  xrhmeo  23555  phtpycc  23600  pcovalg  23621  pcocn  23626  pcohtpylem  23628  pcoass  23633  pcorevlem  23635  ovolunlem1a  24104  ovolunlem1  24105  ioombl1  24170  mbfmax  24257  mbfpos  24259  mbfi1fseqlem2  24324  mbfi1fseq  24329  ditgeq1  24455  ditgeq2  24456  ig1pval  24777  cxpval  25259  lgamgulmlem4  25621  lgamgulmlem5  25622  musumsum  25781  muinv  25782  lgsval  25889  gausslemma2dlem1a  25953  gausslemma2dlem2  25955  gausslemma2dlem3  25956  gausslemma2dlem4  25957  vtxval  26797  iedgval  26798  crctcshwlkn0lem2  27601  crctcshwlkn0lem3  27602  crctcshlem4  27610  crctcsh  27614  clwlkclwwlklem2fv1  27784  eucrct2eupth  28034  psgnfzto1stlem  30796  resvval  30955  smatrcl  31153  smatlem  31154  madjusmdetlem2  31185  madjusmdet  31188  ballotlemsv  31881  ballotlemsf1o  31885  plymulx0  31931  mrsubcv  32871  mrsubrn  32874  rdgprc0  33152  dfrdg2  33154  csbrdgg  34747  csbfinxpg  34806  finxpreclem3  34811  poimirlem2  35058  poimirlem23  35079  poimirlem24  35080  poimirlem27  35083  itg2addnclem3  35109  itgaddnclem2  35115  ftc1anclem5  35133  cdleme27b  37663  cdleme29b  37670  cdleme31sn  37675  cdleme31fv  37685  cdleme40v  37764  dihffval  38525  dihfval  38526  dihval  38527  metakunt3  39349  metakunt4  39350  metakunt6  39352  metakunt7  39353  metakunt8  39354  metakunt10  39356  metakunt11  39357  metakunt12  39358  metakunt20  39366  metakunt21  39367  metakunt22  39368  metakunt32  39378  aomclem8  40002  mnringvald  40918  icccncfext  42526  dvnxpaek  42581  fourierdlem103  42848  fourierdlem104  42849  ioorrnopn  42944  ioorrnopnxr  42946  hsphoival  43215  sge0hsphoire  43225  hoidmvlelem1  43231  hoidmvlelem2  43232  hoidmvlelem3  43233  hoidmvlelem4  43234  hoidmvlelem5  43235  hoidifhspval3  43255  hspmbllem2  43263  ovolval4  43287  afv2eq12d  43768
 Copyright terms: Public domain W3C validator