Theorem elimhyp 4554

Description: Eliminate a hypothesis containing class variable 𝐴 when it is known for a specific class 𝐵. For more information, see comments in dedth 4547. (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 4494	. . . . 5 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
2	1	eqcomd 2735	. . . 4 ⊢ (𝜑 → 𝐴 = if(𝜑, 𝐴, 𝐵))
3		elimhyp.1	. . . 4 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜑 ↔ 𝜓))
4	2, 3	syl 17	. . 3 ⊢ (𝜑 → (𝜑 ↔ 𝜓))
5	4	ibi 267	. 2 ⊢ (𝜑 → 𝜓)
6		elimhyp.3	. . 3 ⊢ 𝜒
7		iffalse 4497	. . . . 5 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)
8	7	eqcomd 2735	. . . 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 4488

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-if 4489

This theorem is referenced by:  elimel  4558  elimf  6687  oeoa  8561  oeoe  8563  limensuc  9118  axcc4dom  10394  elimne0  11164  elimgt0  12020  elimge0  12021  2ndcdisj  23343  siilem2  30781  normlem7tALT  31048  hhsssh  31198  shintcl  31259  chintcl  31261  spanun  31474  elunop2  31942  lnophm  31948  nmbdfnlb  31979  hmopidmch  32082  hmopidmpj  32083  chirred  32324  limsucncmp  36434  elimhyps  38954  elimhyps2  38957