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

Theorem ifeq1da 4307
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 4295 . 2 ((𝜑𝜓) → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
3 iffalse 4286 . . . 4 𝜓 → if(𝜓, 𝐴, 𝐶) = 𝐶)
4 iffalse 4286 . . . 4 𝜓 → if(𝜓, 𝐵, 𝐶) = 𝐶)
53, 4eqtr4d 2836 . . 3 𝜓 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
65adantl 474 . 2 ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
72, 6pm2.61dan 848 1 (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 385   = wceq 1653  ifcif 4277
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2777
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-rab 3098  df-v 3387  df-un 3774  df-if 4278
This theorem is referenced by:  ifeq12da  4309  cantnflem1d  8835  cantnflem1  8836  dfac12lem1  9253  xrmaxeq  12259  xrmineq  12260  rexmul  12350  max0add  14391  sumeq2ii  14764  fsumser  14802  ramcl  16066  dmdprdsplitlem  18752  coe1pwmul  19971  scmatscmiddistr  20640  mulmarep1gsum1  20705  maducoeval2  20772  madugsum  20775  madurid  20776  ptcld  21745  copco  23145  ibllem  23872  itgvallem3  23893  iblposlem  23899  iblss2  23913  iblmulc2  23938  cnplimc  23992  limcco  23998  dvexp3  24082  dchrinvcl  25330  lgsval2lem  25384  lgsval4lem  25385  lgsneg  25398  lgsmod  25400  lgsdilem2  25410  rpvmasum2  25553  mrsubrn  31927  ftc1anclem6  33978  ftc1anclem8  33980
  Copyright terms: Public domain W3C validator