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

Theorem ifeq1da 4499
Description: Conditional equality. (Contributed by Jeff Madsen, 2-Sep-2009.)
Hypothesis
Ref Expression
ifeq1da.1 ((𝜑𝜓) → 𝐴 = 𝐵)
Assertion
Ref Expression
ifeq1da (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))

Proof of Theorem ifeq1da
StepHypRef Expression
1 ifeq1da.1 . . 3 ((𝜑𝜓) → 𝐴 = 𝐵)
21ifeq1d 4487 . 2 ((𝜑𝜓) → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
3 iffalse 4478 . . . 4 𝜓 → if(𝜓, 𝐴, 𝐶) = 𝐶)
4 iffalse 4478 . . . 4 𝜓 → if(𝜓, 𝐵, 𝐶) = 𝐶)
53, 4eqtr4d 2863 . . 3 𝜓 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
65adantl 482 . 2 ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
72, 6pm2.61dan 809 1 (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396   = wceq 1530  ifcif 4469
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-rab 3151  df-v 3501  df-un 3944  df-if 4470
This theorem is referenced by:  ifeq12da  4501  cantnflem1d  9143  cantnflem1  9144  dfac12lem1  9561  xrmaxeq  12565  xrmineq  12566  rexmul  12657  max0add  14663  sumeq2ii  15042  fsumser  15079  ramcl  16357  dmdprdsplitlem  19081  coe1pwmul  20366  scmatscmiddistr  21035  mulmarep1gsum1  21100  maducoeval2  21167  madugsum  21170  madurid  21171  ptcld  22139  ibllem  24282  itgvallem3  24303  iblposlem  24309  iblss2  24323  iblmulc2  24348  cnplimc  24402  limcco  24408  dvexp3  24492  dchrinvcl  25745  lgsval2lem  25799  lgsval4lem  25800  lgsneg  25813  lgsmod  25815  lgsdilem2  25825  rpvmasum2  26004  mrsubrn  32646  ftc1anclem6  34841  ftc1anclem8  34843
  Copyright terms: Public domain W3C validator