Theorem pm5.21ndd 713

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  924  sbcrext  3123  rmob  3139  epelg  4416  eqbrrdva  4930  elrelimasn  5133  relbrcnvg  5146  fmptco  5848  ovelrn  6211  suppcofn  6479  brtpos2  6495  elpmg  6911  brdomg  6998  suppeqfsuppbi  7261  elfi2  7272  genpelvl  7843  genpelvu  7844  fzoval  10504  nninfinf  10829  clim  11991  dvdsaddre2b  12552  pceu  13018  divsfval  13592  sgrppropd  13676  mndpropd  13701  issubg3  13945  resghm2b  14015  rngpropd  14194  dvdsrd  14339  opprsubrngg  14457  subrngpropd  14462  subrgpropd  14499  rhmpropd  14500  lmodprop2d  14622  cnrest2  15227  cnptoprest2  15231  lmss  15237  reopnap  15537  limcdifap  15653  iswlkg  16450  isclwwlkng  16527