Theorem ifbi 4508

Description: Equivalence theorem for conditional operators. (Contributed by Raph Levien, 15-Jan-2004.)

Assertion

Ref	Expression
ifbi	⊢ ((𝜑 ↔ 𝜓) → if(𝜑, 𝐴, 𝐵) = if(𝜓, 𝐴, 𝐵))

Proof of Theorem ifbi

Step	Hyp	Ref	Expression
1		dfbi3 1065	. 2 ⊢ ((𝜑 ↔ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ ¬ 𝜓)))
2		iftrue 4491	. . . 4 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
3		iftrue 4491	. . . . 5 ⊢ (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴)
4	3	eqcomd 2768	. . . 4 ⊢ (𝜓 → 𝐴 = if(𝜓, 𝐴, 𝐵))
5	2, 4	sylan9eq 2817	. . 3 ⊢ ((𝜑 ∧ 𝜓) → if(𝜑, 𝐴, 𝐵) = if(𝜓, 𝐴, 𝐵))
6		iffalse 4494	. . . 4 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)
7		iffalse 4494	. . . . 5 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵)
8	7	eqcomd 2768	. . . 4 ⊢ (¬ 𝜓 → 𝐵 = if(𝜓, 𝐴, 𝐵))
9	6, 8	sylan9eq 2817	. . 3 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → if(𝜑, 𝐴, 𝐵) = if(𝜓, 𝐴, 𝐵))
10	5, 9	jaoi 871	. 2 ⊢ (((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ ¬ 𝜓)) → if(𝜑, 𝐴, 𝐵) = if(𝜓, 𝐴, 𝐵))
11	1, 10	sylbi 220	1 ⊢ ((𝜑 ↔ 𝜓) → if(𝜑, 𝐴, 𝐵) = if(𝜓, 𝐴, 𝐵))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   = wceq 1570  ifcif 4485

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-if 4486

This theorem is used by:  ifbid  4509  ifbieq2i  4511  prodeq1i  16007  psdmvr  22398  gsummoncoe1  22534  scmatscm  22736  mulmarep1gsum1  22796  madugsum  22866  matunitlindflem2  22903  mp2pm2mplem4  23035  dchrhash  27505  lgsdi  27568  rpvmasum2  27746  ifnebib  33010  ififcom  33011  itgeq12i  36813  bj-projval  37727  itg2gt0cn  38411  dedths  39822  dfafv2  48007