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  4437  eqbrrdva  4952  elrelimasn  5156  relbrcnvg  5169  relndmfv  5731  fmptco  5877  ovelrn  6241  suppcofn  6510  brtpos2  6526  elpmg  6942  brdomg  7036  suppeqfsuppbi  7300  elfi2  7311  genpelvl  7885  genpelvu  7886  indval0  9306  fzoval  10572  nninfinf  10901  nn0sqdc  11168  clim  12072  dvdsaddre2b  12633  pceu  13103  divsfval  13708  sgrppropd  13787  mndpropd  13812  issubg3  14054  resghm2b  14124  cntzval  14153  resscntz  14166  rngpropd  14361  dvdsrd  14510  opprsubrngg  14628  subrngpropd  14633  subrgpropd  14670  rhmpropd  14671  lmodprop2d  14794  assapropd  15123  cnrest2  15462  cnptoprest2  15466  lmss  15472  reopnap  15772  limcdifap  15888  iswlkg  16775  isclwwlkng  16852