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  7880  genpelvu  7881  indval0  9300  fzoval  10566  nninfinf  10895  nn0sqdc  11162  clim  12066  dvdsaddre2b  12627  pceu  13097  divsfval  13702  sgrppropd  13781  mndpropd  13806  issubg3  14048  resghm2b  14118  cntzval  14147  resscntz  14160  rngpropd  14338  dvdsrd  14485  opprsubrngg  14603  subrngpropd  14608  subrgpropd  14645  rhmpropd  14646  lmodprop2d  14769  assapropd  15098  cnrest2  15428  cnptoprest2  15432  lmss  15438  reopnap  15738  limcdifap  15854  iswlkg  16736  isclwwlkng  16813