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

Theorem ifbieq12d 4515
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 4510 . 2 (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐴, 𝐵))
3 ifbieq12d.2 . . 3 (𝜑𝐴 = 𝐶)
4 ifbieq12d.3 . . 3 (𝜑𝐵 = 𝐷)
53, 4ifeq12d 4508 . 2 (𝜑 → if(𝜒, 𝐴, 𝐵) = if(𝜒, 𝐶, 𝐷))
62, 5eqtrd 2777 1 (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐶, 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1542  ifcif 4487
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3409  df-v 3448  df-un 3916  df-if 4488
This theorem is referenced by:  csbif  4544  csbopg  4849  tz7.44-2  8354  tz7.44-3  8355  boxcutc  8880  unxpdomlem1  9195  ttrcltr  9653  updjudhcoinlf  9869  updjudhcoinrg  9870  dfac12lem1  10080  dfac12r  10083  fin23lem12  10268  fin23lem33  10282  ttukeylem3  10448  ttukey2g  10453  xaddval  13143  seqf1olem2  13949  expval  13970  ccatfval  14462  ccatval1  14466  ccatval2  14467  ccatalpha  14482  relexpsucnnr  14911  ruclem1  16114  eucalgval2  16458  setsstruct  17049  ressval  17116  gsumvalx  18532  gsumpropd  18534  gsumpropd2lem  18535  gsumress  18538  mulgval  18877  pmtrfv  19235  xrsdsval  20844  mvrfval  21392  selvfval  21530  marrepeval  21915  marepveval  21920  mdetunilem9  21972  madutpos  21994  madugsum  21995  minmar1eval  22001  symgmatr01lem  22005  symgmatr01  22006  gsummatr01lem3  22009  gsummatr01lem4  22010  gsummatr01  22011  ptcmplem3  23408  xrhmeo  24312  phtpycc  24357  pcovalg  24378  pcocn  24383  pcohtpylem  24385  pcoass  24390  pcorevlem  24392  ovolunlem1a  24863  ovolunlem1  24864  ioombl1  24929  mbfmax  25016  mbfpos  25018  mbfi1fseqlem2  25084  mbfi1fseq  25089  ditgeq1  25215  ditgeq2  25216  ig1pval  25540  cxpval  26022  lgamgulmlem4  26384  lgamgulmlem5  26385  musumsum  26544  muinv  26545  lgsval  26652  gausslemma2dlem1a  26716  gausslemma2dlem2  26718  gausslemma2dlem3  26719  gausslemma2dlem4  26720  vtxval  27954  iedgval  27955  crctcshwlkn0lem2  28759  crctcshwlkn0lem3  28760  crctcshlem4  28768  crctcsh  28772  clwlkclwwlklem2fv1  28942  eucrct2eupth  29192  psgnfzto1stlem  31952  resvval  32121  smatrcl  32380  smatlem  32381  madjusmdetlem2  32412  madjusmdet  32415  ballotlemsv  33112  ballotlemsf1o  33116  plymulx0  33162  mrsubcv  34107  mrsubrn  34110  rdgprc0  34371  dfrdg2  34373  csbrdgg  35803  csbfinxpg  35862  finxpreclem3  35867  poimirlem2  36083  poimirlem23  36104  poimirlem24  36105  poimirlem27  36108  itg2addnclem3  36134  itgaddnclem2  36140  ftc1anclem5  36158  cdleme27b  38834  cdleme29b  38841  cdleme31sn  38846  cdleme31fv  38856  cdleme40v  38935  dihffval  39696  dihfval  39697  dihval  39698  metakunt3  40582  metakunt4  40583  metakunt6  40585  metakunt7  40586  metakunt8  40587  metakunt10  40589  metakunt11  40590  metakunt12  40591  metakunt20  40599  metakunt21  40600  metakunt22  40601  metakunt32  40611  prjspnfv01  40965  prjspner01  40966  prjspner1  40967  aomclem8  41391  mnringvald  42495  icccncfext  44135  dvnxpaek  44190  fourierdlem103  44457  fourierdlem104  44458  ioorrnopn  44553  ioorrnopnxr  44555  hsphoival  44827  sge0hsphoire  44837  hoidmvlelem1  44843  hoidmvlelem2  44844  hoidmvlelem3  44845  hoidmvlelem4  44846  hoidmvlelem5  44847  hoidifhspval3  44867  hspmbllem2  44875  ovolval4  44899  afv2eq12d  45454
  Copyright terms: Public domain W3C validator