Theorem elimhyp 2386

Description: Eliminate a hypothesis containing class variable A when it is known for a specific class B. For more information, see comments in dedth 2379.

Hypotheses

Ref	Expression
elimhyp.1	⊢ (A = if(φ, A, B) → (φ ↔ ψ))
elimhyp.2	⊢ (B = if(φ, A, B) → (χ ↔ ψ))
elimhyp.3	⊢ χ

Assertion

Ref	Expression
elimhyp	⊢ ψ

Proof of Theorem elimhyp

Step	Hyp	Ref	Expression
1		iftrue 2362	. . . . 5 ⊢ (φ → if(φ, A, B) = A)
2	1	eqcomd 1477	. . . 4 ⊢ (φ → A = if(φ, A, B))
3		elimhyp.1	. . . 4 ⊢ (A = if(φ, A, B) → (φ ↔ ψ))
4	2, 3	syl 10	. . 3 ⊢ (φ → (φ ↔ ψ))
5	4	ibi 591	. 2 ⊢ (φ → ψ)
6		elimhyp.3	. . 3 ⊢ χ
7		iffalse 2363	. . . . 5 ⊢ (¬ φ → if(φ, A, B) = B)
8	7	eqcomd 1477	. . . 4 ⊢ (¬ φ → B = if(φ, A, B))
9		elimhyp.2	. . . 4 ⊢ (B = if(φ, A, B) → (χ ↔ ψ))
10	8, 9	syl 10	. . 3 ⊢ (¬ φ → (χ ↔ ψ))
11	6, 10	mpbii 193	. 2 ⊢ (¬ φ → ψ)
12	5, 11	pm2.61i 126	1 ⊢ ψ

Syntax hints:  ¬ wn 2   → wi 3   ↔ wb 146   = wceq 954   ifcif 2357

This theorem is referenced by:  elimel 2390  elimf 3618  limensuc 4493  elimne0 5296  div11t 5729  recrect 5740  elimgt0 5773  elimge0 5774  sqrlem20 6630  sqrlem21 6631  sqrlem22 6632  caucvg3t 7112  expcnvlem5 7174  geolim 7180  geolim1 7182  efseq1ex 7256  ef1tlub 7332  absef01tlub 7337  eflegeot 7364  efm1legeot 7366  efcnlem4 7370  reeff1olem2 7373  reeff1olem2OLD 7375  bcth 7982  siilem2 8456  normlem7tALT 8924  hhsssh 9078  occlt 9121  shintclt 9232  chintclt 9234  spanunt 9406  elunop2t 9876  lnophmt 9882  nmbdfnlbt 9917  hmopidmcht 10019  hmopidmpjt 10020  irredt 10259  erdisj2 10379

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-if 2358

Copyright terms: Public domain