Theorem pm5.21ndd 706

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  917  sbcrext  3055  rmob  3070  epelg  4308  eqbrrdva  4815  elrelimasn  5012  relbrcnvg  5025  fmptco  5703  ovelrn  6045  brtpos2  6276  elpmg  6690  brdomg  6774  elfi2  7001  genpelvl  7541  genpelvu  7542  fzoval  10178  clim  11321  dvdsaddre2b  11880  pceu  12327  sgrppropd  12876  mndpropd  12901  issubg3  13131  resghm2b  13201  rngpropd  13309  dvdsrd  13444  opprsubrngg  13558  subrngpropd  13563  subrgpropd  13595  lmodprop2d  13664  cnrest2  14193  cnptoprest2  14197  lmss  14203  reopnap  14495  limcdifap  14588