Theorem pm5.21ndd 707

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  918  sbcrext  3084  rmob  3100  epelg  4356  eqbrrdva  4867  elrelimasn  5068  relbrcnvg  5081  fmptco  5771  ovelrn  6120  brtpos2  6362  elpmg  6776  brdomg  6862  elfi2  7102  genpelvl  7662  genpelvu  7663  fzoval  10307  nninfinf  10627  clim  11753  dvdsaddre2b  12313  pceu  12779  divsfval  13321  sgrppropd  13406  mndpropd  13433  issubg3  13689  resghm2b  13759  rngpropd  13878  dvdsrd  14017  opprsubrngg  14134  subrngpropd  14139  subrgpropd  14176  rhmpropd  14177  lmodprop2d  14271  cnrest2  14869  cnptoprest2  14873  lmss  14879  reopnap  15179  limcdifap  15295