Theorem elimhyp 4558

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   = wceq 1567  ifcif 4492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-if 4493

This theorem is referenced by:  elimel  4562  elimf  6705  oeoa  8583  oeoe  8585  limensuc  9142  axcc4dom  10425  elimne0  11196  elimgt0  12053  elimge0  12054  2ndcdisj  23582  siilem2  31145  normlem7tALT  31412  hhsssh  31562  shintcl  31623  chintcl  31625  spanun  31838  elunop2  32306  lnophm  32312  nmbdfnlb  32343  hmopidmch  32446  hmopidmpj  32447  chirred  32688  limsucncmp  36880  elimhyps  39659  elimhyps2  39662