Theorem elimhyp 3021

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

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 2989	. . . . 5 |- (ph -> if(ph, A, B) = A)
2	1	eqcomd 1889	. . . 4 |- (ph -> A = if(ph, A, B))
3		elimhyp.1	. . . 4 |- (A = if(ph, A, B) -> (ph <-> ps))
4	2, 3	syl 12	. . 3 |- (ph -> (ph <-> ps))
5	4	ibi 652	. 2 |- (ph -> ps)
6		elimhyp.3	. . 3 |- ch
7		iffalse 2991	. . . . 5 |- (-. ph -> if(ph, A, B) = B)
8	7	eqcomd 1889	. . . 4 |- (-. ph -> B = if(ph, A, B))
9		elimhyp.2	. . . 4 |- (B = if(ph, A, B) -> (ch <-> ps))
10	8, 9	syl 12	. . 3 |- (-. ph -> (ch <-> ps))
11	6, 10	mpbii 210	. 2 |- (-. ph -> ps)
12	5, 11	pm2.61i 140	1 |- ps

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   = wceq 1298  ifcif 2982

This theorem is referenced by:  elimel 3025  elimf 4561  oeoa 5272  oeoe 5274  limensuc 5601  elimne0 6469  div11 6941  recrec 6952  elimgt0 6987  elimge0 6988  sqrlem20 7942  sqrlem21 7943  sqrlem22 7944  caucvg3 8428  expcnvlem5 8492  geolim 8499  geolim1 8501  efseq1ex 8568  ef1tlubi 8644  absef01tlubi 8650  eflegeo 8681  efm1legeo 8683  efcnlem4 8687  reeff1olem2 8690  bcth 9310  vacnlem4 9670  siilem2 9853  erdisj2 10164  normlem7tALT 10618  hhsssh 10772  occl 10815  shintcl 10927  chintcl 10929  spanun 11101  elunop2 11575  lnophm 11581  nmbdfnlb 11616  hmopidmch 11725  hmopidmpj 11726  irred 11967  erthdmg 15730  fimaxg 15747  supclt 15762  supubt 15763  supeut 15767  fsumltisumi 15823  fsumleisumi 15826  bfplem11 16008  bfp 16009

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-10 1308  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-if 2983

Copyright terms: Public domain