Theorem ifeq1d 4243

Description: Equality deduction for conditional operator. (Contributed by NM, 16-Feb-2005.)

Hypothesis

Ref	Expression
ifeq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
ifeq1d	⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))

Proof of Theorem ifeq1d

Step	Hyp	Ref	Expression
1		ifeq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		ifeq1 4229	. 2 ⊢ (𝐴 = 𝐵 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
3	1, 2	syl 17	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))

Syntax hints:   → wi 4   = wceq 1631  ifcif 4225

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-rab 3070  df-v 3353  df-un 3728  df-if 4226

This theorem is referenced by:  ifeq12d  4245  ifbieq1d  4248  ifeq1da  4255  rabsnif  4394  fsuppmptif  8461  cantnflem1  8750  sumeq2w  14630  cbvsum  14633  isumless  14784  prodss  14884  subgmulg  17816  evlslem2  19727  dmatcrng  20526  scmatscmiddistr  20532  scmatcrng  20545  marrepfval  20584  mdetr0  20629  mdetunilem8  20643  madufval  20661  madugsum  20667  minmar1fval  20670  decpmatid  20795  monmatcollpw  20804  pmatcollpwscmatlem1  20814  cnmpt2pc  22947  pcoval2  23035  pcopt  23041  itgz  23767  iblss2  23792  itgss  23798  itgcn  23829  plyeq0lem  24186  dgrcolem2  24250  plydivlem4  24271  leibpi  24890  chtublem  25157  sumdchr  25218  bposlem6  25235  lgsval  25247  dchrvmasumiflem2  25412  padicabvcxp  25542  dfrdg3  32038  matunitlindflem1  33738  ftc1anclem2  33818  ftc1anclem5  33821  ftc1anclem7  33823  hoidifhspval  41342  hoimbl  41365