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  3110  rmob  3126  epelg  4393  eqbrrdva  4906  elrelimasn  5109  relbrcnvg  5122  fmptco  5821  ovelrn  6181  suppcofn  6444  brtpos2  6460  elpmg  6876  brdomg  6962  elfi2  7214  genpelvl  7775  genpelvu  7776  fzoval  10428  nninfinf  10751  clim  11904  dvdsaddre2b  12465  pceu  12931  divsfval  13474  sgrppropd  13559  mndpropd  13586  issubg3  13842  resghm2b  13912  rngpropd  14032  dvdsrd  14172  opprsubrngg  14289  subrngpropd  14294  subrgpropd  14331  rhmpropd  14332  lmodprop2d  14427  cnrest2  15030  cnptoprest2  15034  lmss  15040  reopnap  15340  limcdifap  15456  iswlkg  16253  isclwwlkng  16330