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

Theorem ifeq1da 4066
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 4054 . 2 ((𝜑𝜓) → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
3 iffalse 4045 . . . 4 𝜓 → if(𝜓, 𝐴, 𝐶) = 𝐶)
4 iffalse 4045 . . . 4 𝜓 → if(𝜓, 𝐵, 𝐶) = 𝐶)
53, 4eqtr4d 2647 . . 3 𝜓 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
65adantl 481 . 2 ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
72, 6pm2.61dan 828 1 (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 383   = wceq 1475  ifcif 4036
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-un 3545  df-if 4037
This theorem is referenced by:  ifeq12da  4068  cantnflem1d  8468  cantnflem1  8469  dfac12lem1  8848  xrmaxeq  11884  xrmineq  11885  rexmul  11973  max0add  13898  sumeq2ii  14271  fsumser  14308  ramcl  15571  dmdprdsplitlem  18259  coe1pwmul  19470  scmatscmiddistr  20133  mulmarep1gsum1  20198  maducoeval2  20265  madugsum  20268  madurid  20269  ptcld  21226  copco  22626  ibllem  23337  itgvallem3  23358  iblposlem  23364  iblss2  23378  iblmulc2  23403  cnplimc  23457  limcco  23463  dvexp3  23545  dchrinvcl  24778  lgsval2lem  24832  lgsval4lem  24833  lgsneg  24846  lgsmod  24848  lgsdilem2  24858  rpvmasum2  25001  mrsubrn  30664  ftc1anclem6  32660  ftc1anclem8  32662
  Copyright terms: Public domain W3C validator