Theorem elimhyp 4444

Description: Eliminate a hypothesis containing class variable 𝐴 when it is known for a specific class 𝐵. For more information, see comments in dedth 4437. (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 4387	. . . . 5 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
2	1	eqcomd 2801	. . . 4 ⊢ (𝜑 → 𝐴 = if(𝜑, 𝐴, 𝐵))
3		elimhyp.1	. . . 4 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜑 ↔ 𝜓))
4	2, 3	syl 17	. . 3 ⊢ (𝜑 → (𝜑 ↔ 𝜓))
5	4	ibi 268	. 2 ⊢ (𝜑 → 𝜓)
6		elimhyp.3	. . 3 ⊢ 𝜒
7		iffalse 4390	. . . . 5 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)
8	7	eqcomd 2801	. . . 4 ⊢ (¬ 𝜑 → 𝐵 = if(𝜑, 𝐴, 𝐵))
9		elimhyp.2	. . . 4 ⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒 ↔ 𝜓))
10	8, 9	syl 17	. . 3 ⊢ (¬ 𝜑 → (𝜒 ↔ 𝜓))
11	6, 10	mpbii 234	. 2 ⊢ (¬ 𝜑 → 𝜓)
12	5, 11	pm2.61i 183	1 ⊢ 𝜓

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   = wceq 1522  ifcif 4381

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-ex 1762  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-if 4382

This theorem is referenced by:  elimel  4448  elimf  6381  oeoa  8073  oeoe  8075  limensuc  8541  axcc4dom  9709  elimne0  10477  elimgt0  11326  elimge0  11327  2ndcdisj  21748  siilem2  28320  normlem7tALT  28587  hhsssh  28737  shintcl  28798  chintcl  28800  spanun  29013  elunop2  29481  lnophm  29487  nmbdfnlb  29518  hmopidmch  29621  hmopidmpj  29622  chirred  29863  limsucncmp  33403  elimhyps  35628  elimhyps2  35631