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  4381  eqbrrdva  4892  elrelimasn  5094  relbrcnvg  5107  fmptco  5803  ovelrn  6160  brtpos2  6403  elpmg  6819  brdomg  6905  elfi2  7150  genpelvl  7710  genpelvu  7711  fzoval  10356  nninfinf  10677  clim  11807  dvdsaddre2b  12367  pceu  12833  divsfval  13376  sgrppropd  13461  mndpropd  13488  issubg3  13744  resghm2b  13814  rngpropd  13933  dvdsrd  14073  opprsubrngg  14190  subrngpropd  14195  subrgpropd  14232  rhmpropd  14233  lmodprop2d  14327  cnrest2  14925  cnptoprest2  14929  lmss  14935  reopnap  15235  limcdifap  15351  iswlkg  16070