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  3080  rmob  3095  epelg  4345  eqbrrdva  4856  elrelimasn  5057  relbrcnvg  5070  fmptco  5759  ovelrn  6108  brtpos2  6350  elpmg  6764  brdomg  6850  elfi2  7089  genpelvl  7645  genpelvu  7646  fzoval  10290  nninfinf  10610  clim  11667  dvdsaddre2b  12227  pceu  12693  divsfval  13235  sgrppropd  13320  mndpropd  13347  issubg3  13603  resghm2b  13673  rngpropd  13792  dvdsrd  13931  opprsubrngg  14048  subrngpropd  14053  subrgpropd  14090  rhmpropd  14091  lmodprop2d  14185  cnrest2  14783  cnptoprest2  14787  lmss  14793  reopnap  15093  limcdifap  15209