Theorem elimhyp 4547

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   = 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:  elimel  4551  elimf  6708  oeoa  8609  oeoe  8611  limensuc  9176  axcc4dom  10522  elimne0  11299  elimgt0  12158  elimge0  12159  2ndcdisj  23780  siilem2  31459  normlem7tALT  31726  hhsssh  31876  shintcl  31937  chintcl  31939  spanun  32152  elunop2  32620  lnophm  32626  nmbdfnlb  32657  hmopidmch  32760  hmopidmpj  32761  chirred  33002  limsucncmp  37326  elimhyps  40111  elimhyps2  40114