Theorem elimhyp 2380

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

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 2356	. . . . 5 |- (ph -> if(ph, A, B) = A)
2	1	eqcomd 1472	. . . 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 590	. 2 |- (ph -> ps)
6		elimhyp.3	. . 3 |- ch
7		iffalse 2357	. . . . 5 |- (-. ph -> if(ph, A, B) = B)
8	7	eqcomd 1472	. . . 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 953  ifcif 2351

This theorem is referenced by:  elimel 2384  elimf 3612  limensuc 4487  elimne0 5288  div11t 5721  recrect 5732  elimgt0 5765  elimge0 5766  sqrlem20 6622  sqrlem21 6623  sqrlem22 6624  caucvg3t 7104  expcnvlem5 7166  geolim 7172  geolim1 7174  efseq1ex 7248  ef1tlub 7324  absef01tlub 7329  eflegeot 7356  efm1legeot 7358  efcnlem4 7362  reeff1olem2 7365  reeff1olem2OLD 7367  bcth 7966  siilem2 8443  normlem7tALT 8906  hhsssh 9059  occlt 9098  shintclt 9209  chintclt 9211  spanunt 9383  elunop2t 9853  lnophmt 9859  nmbdfnlbt 9894  hmopidmcht 9992  hmopidmpjt 9993  irredt 10230  erdisj2 10343

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-if 2352

Copyright terms: Public domain