Theorem pm5.21ndd 713

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  924  sbcrext  3120  rmob  3136  epelg  4411  eqbrrdva  4925  elrelimasn  5128  relbrcnvg  5141  fmptco  5843  ovelrn  6203  suppcofn  6466  brtpos2  6482  elpmg  6898  brdomg  6985  suppeqfsuppbi  7248  elfi2  7259  genpelvl  7827  genpelvu  7828  fzoval  10482  nninfinf  10805  clim  11966  dvdsaddre2b  12527  pceu  12993  divsfval  13541  sgrppropd  13626  mndpropd  13653  issubg3  13909  resghm2b  13979  rngpropd  14099  dvdsrd  14239  opprsubrngg  14356  subrngpropd  14361  subrgpropd  14398  rhmpropd  14399  lmodprop2d  14496  cnrest2  15101  cnptoprest2  15105  lmss  15111  reopnap  15411  limcdifap  15527  iswlkg  16324  isclwwlkng  16401