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  3106  rmob  3122  epelg  4380  eqbrrdva  4891  elrelimasn  5093  relbrcnvg  5106  fmptco  5800  ovelrn  6153  brtpos2  6395  elpmg  6809  brdomg  6895  elfi2  7135  genpelvl  7695  genpelvu  7696  fzoval  10340  nninfinf  10660  clim  11787  dvdsaddre2b  12347  pceu  12813  divsfval  13356  sgrppropd  13441  mndpropd  13468  issubg3  13724  resghm2b  13794  rngpropd  13913  dvdsrd  14052  opprsubrngg  14169  subrngpropd  14174  subrgpropd  14211  rhmpropd  14212  lmodprop2d  14306  cnrest2  14904  cnptoprest2  14908  lmss  14914  reopnap  15214  limcdifap  15330  iswlkg  16032