Theorem pm5.21ndd 705

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  916  sbcrext  3040  rmob  3055  epelg  4290  eqbrrdva  4797  elrelimasn  4994  relbrcnvg  5007  fmptco  5682  ovelrn  6022  brtpos2  6251  elpmg  6663  brdomg  6747  elfi2  6970  genpelvl  7510  genpelvu  7511  fzoval  10147  clim  11288  dvdsaddre2b  11847  pceu  12294  mndpropd  12840  issubg3  13050  dvdsrd  13261  subrgpropd  13367  cnrest2  13706  cnptoprest2  13710  lmss  13716  reopnap  14008  limcdifap  14101