Theorem ifbi 4504

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 4487	. . . 4 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
3		iftrue 4487	. . . . 5 ⊢ (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴)
4	3	eqcomd 2766	. . . 4 ⊢ (𝜓 → 𝐴 = if(𝜓, 𝐴, 𝐵))
5	2, 4	sylan9eq 2815	. . 3 ⊢ ((𝜑 ∧ 𝜓) → if(𝜑, 𝐴, 𝐵) = if(𝜓, 𝐴, 𝐵))
6		iffalse 4490	. . . 4 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)
7		iffalse 4490	. . . . 5 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵)
8	7	eqcomd 2766	. . . 4 ⊢ (¬ 𝜓 → 𝐵 = if(𝜓, 𝐴, 𝐵))
9	6, 8	sylan9eq 2815	. . 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 1569  ifcif 4481

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-if 4482

This theorem is used by:  ifbid  4505  ifbieq2i  4507  prodeq1i  16085  psdmvr  22490  gsummoncoe1  22626  scmatscm  22828  mulmarep1gsum1  22888  madugsum  22958  matunitlindflem2  22995  mp2pm2mplem4  23127  dchrhash  27598  lgsdi  27661  rpvmasum2  27839  ifnebib  33187  ififcom  33188  itgeq12i  37037  bj-projval  37951  itg2gt0cn  38636  dedths  40062  dfafv2  48245