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  6171  brtpos2  6417  elpmg  6833  brdomg  6919  elfi2  7171  genpelvl  7732  genpelvu  7733  fzoval  10383  nninfinf  10706  clim  11846  dvdsaddre2b  12407  pceu  12873  divsfval  13416  sgrppropd  13501  mndpropd  13528  issubg3  13784  resghm2b  13854  rngpropd  13974  dvdsrd  14114  opprsubrngg  14231  subrngpropd  14236  subrgpropd  14273  rhmpropd  14274  lmodprop2d  14368  cnrest2  14966  cnptoprest2  14970  lmss  14976  reopnap  15276  limcdifap  15392  iswlkg  16186  isclwwlkng  16263