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

Theorem ifeq1da 4522
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 4510 . 2 ((𝜑𝜓) → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
3 iffalse 4500 . . . 4 𝜓 → if(𝜓, 𝐴, 𝐶) = 𝐶)
4 iffalse 4500 . . . 4 𝜓 → if(𝜓, 𝐵, 𝐶) = 𝐶)
53, 4eqtr4d 2780 . . 3 𝜓 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
65adantl 483 . 2 ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
72, 6pm2.61dan 812 1 (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 397   = wceq 1542  ifcif 4491
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 3411  df-v 3450  df-un 3920  df-if 4492
This theorem is referenced by:  ifeq12da  4524  cantnflem1d  9631  cantnflem1  9632  dfac12lem1  10086  xrmaxeq  13105  xrmineq  13106  rexmul  13197  max0add  15202  sumeq2ii  15585  fsumser  15622  ramcl  16908  dmdprdsplitlem  19823  coe1pwmul  21666  scmatscmiddistr  21873  mulmarep1gsum1  21938  maducoeval2  22005  madugsum  22008  madurid  22009  ptcld  22980  ibllem  25145  itgvallem3  25166  iblposlem  25172  iblss2  25186  iblmulc2  25211  cnplimc  25267  limcco  25273  dvexp3  25358  dchrinvcl  26617  lgsval2lem  26671  lgsval4lem  26672  lgsneg  26685  lgsmod  26687  lgsdilem2  26697  rpvmasum2  26876  mrsubrn  34147  ftc1anclem6  36185  ftc1anclem8  36187  fsuppind  40794
  Copyright terms: Public domain W3C validator