Theorem pm5.21ndd 710

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  921  sbcrext  3107  rmob  3123  epelg  4385  eqbrrdva  4898  elrelimasn  5100  relbrcnvg  5113  fmptco  5809  ovelrn  6166  brtpos2  6412  elpmg  6828  brdomg  6914  elfi2  7162  genpelvl  7722  genpelvu  7723  fzoval  10373  nninfinf  10695  clim  11832  dvdsaddre2b  12392  pceu  12858  divsfval  13401  sgrppropd  13486  mndpropd  13513  issubg3  13769  resghm2b  13839  rngpropd  13958  dvdsrd  14098  opprsubrngg  14215  subrngpropd  14220  subrgpropd  14257  rhmpropd  14258  lmodprop2d  14352  cnrest2  14950  cnptoprest2  14954  lmss  14960  reopnap  15260  limcdifap  15376  iswlkg  16126  isclwwlkng  16201