Theorem elimhyp 2390

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

Hypotheses

Ref	Expression
elimhyp.1	|- (A = if(ph, A, B) -> (ph <-> ps))
elimhyp.2	|- (B = if(ph, A, B) -> (ch <-> ps))
elimhyp.3	|- ch

Assertion

Ref	Expression
elimhyp	|- ps

Proof of Theorem elimhyp

Step	Hyp	Ref	Expression
1		iftrue 2366	. . . . 5 |- (ph -> if(ph, A, B) = A)
2	1	eqcomd 1480	. . . 4 |- (ph -> A = if(ph, A, B))
3		elimhyp.1	. . . 4 |- (A = if(ph, A, B) -> (ph <-> ps))
4	2, 3	syl 10	. . 3 |- (ph -> (ph <-> ps))
5	4	ibi 592	. 2 |- (ph -> ps)
6		elimhyp.3	. . 3 |- ch
7		iffalse 2367	. . . . 5 |- (-. ph -> if(ph, A, B) = B)
8	7	eqcomd 1480	. . . 4 |- (-. ph -> B = if(ph, A, B))
9		elimhyp.2	. . . 4 |- (B = if(ph, A, B) -> (ch <-> ps))
10	8, 9	syl 10	. . 3 |- (-. ph -> (ch <-> ps))
11	6, 10	mpbii 193	. 2 |- (-. ph -> ps)
12	5, 11	pm2.61i 126	1 |- ps

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146   = wceq 956  ifcif 2361

This theorem is referenced by:  elimel 2394  elimf 3626  limensuc 4507  elimne0 5316  div11t 5765  recrect 5776  elimgt0 5809  elimge0 5810  sqrlem20 6692  sqrlem21 6693  sqrlem22 6694  caucvg3t 7168  expcnvlem5 7231  geolim 7237  geolim1 7239  efseq1ex 7306  ef1tlub 7382  absef01tlub 7388  eflegeot 7416  efm1legeot 7418  efcnlem4 7422  reeff1olem2 7425  bcth 8032  siilem2 8512  normlem7tALT 8985  hhsssh 9139  occlt 9182  shintclt 9294  chintclt 9296  spanunt 9468  elunop2t 9938  lnophmt 9944  nmbdfnlbt 9979  hmopidmcht 10081  hmopidmpjt 10082  irredt 10322  erdisj2 10442

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-if 2362

Copyright terms: Public domain