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

Theorem ifeq1da 4451
 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 4439 . 2 ((𝜑𝜓) → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
3 iffalse 4429 . . . 4 𝜓 → if(𝜓, 𝐴, 𝐶) = 𝐶)
4 iffalse 4429 . . . 4 𝜓 → if(𝜓, 𝐵, 𝐶) = 𝐶)
53, 4eqtr4d 2796 . . 3 𝜓 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
65adantl 485 . 2 ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
72, 6pm2.61dan 812 1 (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   = wceq 1538  ifcif 4420 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 2113  ax-9 2121  ax-10 2142  ax-12 2175  ax-ext 2729 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-rab 3079  df-v 3411  df-un 3863  df-if 4421 This theorem is referenced by:  ifeq12da  4453  cantnflem1d  9184  cantnflem1  9185  dfac12lem1  9603  xrmaxeq  12613  xrmineq  12614  rexmul  12705  max0add  14718  sumeq2ii  15098  fsumser  15135  ramcl  16420  dmdprdsplitlem  19227  coe1pwmul  21003  scmatscmiddistr  21208  mulmarep1gsum1  21273  maducoeval2  21340  madugsum  21343  madurid  21344  ptcld  22313  ibllem  24464  itgvallem3  24485  iblposlem  24491  iblss2  24505  iblmulc2  24530  cnplimc  24586  limcco  24592  dvexp3  24677  dchrinvcl  25936  lgsval2lem  25990  lgsval4lem  25991  lgsneg  26004  lgsmod  26006  lgsdilem2  26016  rpvmasum2  26195  mrsubrn  32991  ftc1anclem6  35437  ftc1anclem8  35439  fsuppind  39806
 Copyright terms: Public domain W3C validator