Theorem pm5.21ndd 717

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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  pm5.21nd  928  sbcrext  3129  rmob  3145  epelg  4435  eqbrrdva  4950  elrelimasn  5153  relbrcnvg  5166  relndmfv  5728  fmptco  5874  ovelrn  6238  suppcofn  6506  brtpos2  6522  elpmg  6938  brdomg  7032  suppeqfsuppbi  7295  elfi2  7306  genpelvl  7879  genpelvu  7880  indval0  9297  fzoval  10555  nninfinf  10880  clim  12047  dvdsaddre2b  12608  pceu  13074  divsfval  13649  sgrppropd  13728  mndpropd  13753  issubg3  13995  resghm2b  14065  rngpropd  14254  dvdsrd  14401  opprsubrngg  14519  subrngpropd  14524  subrgpropd  14561  rhmpropd  14562  lmodprop2d  14685  assapropd  15014  cnrest2  15337  cnptoprest2  15341  lmss  15347  reopnap  15647  limcdifap  15763  iswlkg  16570  isclwwlkng  16647