Theorem elimhyp 4146

Description: Eliminate a hypothesis containing class variable A when it is known for a specific class B. For more information, see comments in dedth 4139. (Contributed by NM, 15-May-1999.)

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 4092	. . . . 5 |- ( ph -> if ( ph , A , B ) = A )
2	1	eqcomd 2628	. . . 4 |- ( ph -> A = if ( ph , A , B ) )
3		elimhyp.1	. . . 4 |- ( A = if ( ph , A , B ) -> ( ph <-> ps ) )
4	2, 3	syl 17	. . 3 |- ( ph -> ( ph <-> ps ) )
5	4	ibi 256	. 2 |- ( ph -> ps )
6		elimhyp.3	. . 3 |- ch
7		iffalse 4095	. . . . 5 |- ( -. ph -> if ( ph , A , B ) = B )
8	7	eqcomd 2628	. . . 4 |- ( -. ph -> B = if ( ph , A , B ) )
9		elimhyp.2	. . . 4 |- ( B = if ( ph , A , B ) -> ( ch <-> ps ) )
10	8, 9	syl 17	. . 3 |- ( -. ph -> ( ch <-> ps ) )
11	6, 10	mpbii 223	. 2 |- ( -. ph -> ps )
12	5, 11	pm2.61i 176	1 |- ps

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   = wceq 1483   ifcif 4086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-if 4087

This theorem is referenced by:  elimel  4150  elimf  6044  oeoa  7677  oeoe  7679  limensuc  8137  axcc4dom  9263  elimne0  10030  elimgt0  10859  elimge0  10860  2ndcdisj  21259  siilem2  27707  normlem7tALT  27976  hhsssh  28126  shintcl  28189  chintcl  28191  spanun  28404  elunop2  28872  lnophm  28878  nmbdfnlb  28909  hmopidmch  29012  hmopidmpj  29013  chirred  29254  limsucncmp  32445  elimhyps  34247  elimhyps2  34250