Theorem elimhyp 4590

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   = wceq 1534  ifcif 4525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-if 4526

This theorem is referenced by:  elimel  4594  elimf  6716  oeoa  8612  oeoe  8614  limensuc  9173  axcc4dom  10459  elimne0  11229  elimgt0  12077  elimge0  12078  2ndcdisj  23354  siilem2  30656  normlem7tALT  30923  hhsssh  31073  shintcl  31134  chintcl  31136  spanun  31349  elunop2  31817  lnophm  31823  nmbdfnlb  31854  hmopidmch  31957  hmopidmpj  31958  chirred  32199  limsucncmp  35925  elimhyps  38428  elimhyps2  38431