Theorem pm5.21ndd 717

Description: Eliminate an antecedent implied by each side of a biconditional, deduction version. (Contributed by Paul Chapman, 21-Nov-2012.) (Revised by Mario Carneiro, 31-Jan-2015.)

Hypotheses

Ref	Expression
pm5.21ndd.1	|- ( ph -> ( ch -> ps ) )
pm5.21ndd.2	|- ( ph -> ( th -> ps ) )
pm5.21ndd.3	|- ( ph -> ( ps -> ( ch <-> th ) ) )

Assertion

Ref	Expression
pm5.21ndd	|- ( ph -> ( ch <-> th ) )

Proof of Theorem pm5.21ndd

Step	Hyp	Ref	Expression
1		pm5.21ndd.1	. . . 4 |- ( ph -> ( ch -> ps ) )
2		pm5.21ndd.3	. . . 4 |- ( ph -> ( ps -> ( ch <-> th ) ) )
3	1, 2	syld 45	. . 3 |- ( ph -> ( ch -> ( ch <-> th ) ) )
4	3	ibd 178	. 2 |- ( ph -> ( ch -> th ) )
5		pm5.21ndd.2	. . . . 5 |- ( ph -> ( th -> ps ) )
6	5, 2	syld 45	. . . 4 |- ( ph -> ( th -> ( ch <-> th ) ) )
7		bicom1 131	. . . 4 |- ( ( ch <-> th ) -> ( th <-> ch ) )
8	6, 7	syl6 33	. . 3 |- ( ph -> ( th -> ( th <-> ch ) ) )
9	8	ibd 178	. 2 |- ( ph -> ( th -> ch ) )
10	4, 9	impbid 129	1 |- ( ph -> ( ch <-> th ) )

Syntax hints:   -> wi 4   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm5.21nd  928  sbcrext  3129  rmob  3145  epelg  4430  eqbrrdva  4945  elrelimasn  5148  relbrcnvg  5161  fmptco  5865  ovelrn  6228  suppcofn  6496  brtpos2  6512  elpmg  6928  brdomg  7022  suppeqfsuppbi  7285  elfi2  7296  genpelvl  7869  genpelvu  7870  fzoval  10533  nninfinf  10858  clim  12025  dvdsaddre2b  12586  pceu  13052  divsfval  13626  sgrppropd  13705  mndpropd  13730  issubg3  13972  resghm2b  14042  rngpropd  14229  dvdsrd  14374  opprsubrngg  14492  subrngpropd  14497  subrgpropd  14534  rhmpropd  14535  lmodprop2d  14657  cnrest2  15260  cnptoprest2  15264  lmss  15270  reopnap  15570  limcdifap  15686  iswlkg  16484  isclwwlkng  16561