Theorem pm5.21ndd 712

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  923  sbcrext  3109  rmob  3125  epelg  4387  eqbrrdva  4900  elrelimasn  5102  relbrcnvg  5115  fmptco  5813  ovelrn  6170  brtpos2  6416  elpmg  6832  brdomg  6918  elfi2  7170  genpelvl  7731  genpelvu  7732  fzoval  10382  nninfinf  10704  clim  11841  dvdsaddre2b  12401  pceu  12867  divsfval  13410  sgrppropd  13495  mndpropd  13522  issubg3  13778  resghm2b  13848  rngpropd  13967  dvdsrd  14107  opprsubrngg  14224  subrngpropd  14229  subrgpropd  14266  rhmpropd  14267  lmodprop2d  14361  cnrest2  14959  cnptoprest2  14963  lmss  14969  reopnap  15269  limcdifap  15385  iswlkg  16179  isclwwlkng  16256