Theorem elimhyp 4566

Description: Eliminate a hypothesis containing class variable 𝐴 when it is known for a specific class 𝐵. For more information, see comments in dedth 4559. (Contributed by NM, 15-May-1999.)

Hypotheses

Ref	Expression
elimhyp.1	⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜑 ↔ 𝜓))
elimhyp.2	⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒 ↔ 𝜓))
elimhyp.3	⊢ 𝜒

Assertion

Ref	Expression
elimhyp	⊢ 𝜓

Proof of Theorem elimhyp

Step	Hyp	Ref	Expression
1		iftrue 4506	. . . . 5 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
2	1	eqcomd 2741	. . . 4 ⊢ (𝜑 → 𝐴 = if(𝜑, 𝐴, 𝐵))
3		elimhyp.1	. . . 4 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜑 ↔ 𝜓))
4	2, 3	syl 17	. . 3 ⊢ (𝜑 → (𝜑 ↔ 𝜓))
5	4	ibi 267	. 2 ⊢ (𝜑 → 𝜓)
6		elimhyp.3	. . 3 ⊢ 𝜒
7		iffalse 4509	. . . . 5 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)
8	7	eqcomd 2741	. . . 4 ⊢ (¬ 𝜑 → 𝐵 = if(𝜑, 𝐴, 𝐵))
9		elimhyp.2	. . . 4 ⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒 ↔ 𝜓))
10	8, 9	syl 17	. . 3 ⊢ (¬ 𝜑 → (𝜒 ↔ 𝜓))
11	6, 10	mpbii 233	. 2 ⊢ (¬ 𝜑 → 𝜓)
12	5, 11	pm2.61i 182	1 ⊢ 𝜓

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   = wceq 1540  ifcif 4500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-if 4501

This theorem is referenced by:  elimel  4570  elimf  6705  oeoa  8609  oeoe  8611  limensuc  9168  axcc4dom  10455  elimne0  11225  elimgt0  12079  elimge0  12080  2ndcdisj  23394  siilem2  30833  normlem7tALT  31100  hhsssh  31250  shintcl  31311  chintcl  31313  spanun  31526  elunop2  31994  lnophm  32000  nmbdfnlb  32031  hmopidmch  32134  hmopidmpj  32135  chirred  32376  limsucncmp  36464  elimhyps  38979  elimhyps2  38982