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  9299  fzoval  10565  nninfinf  10893  nn0sqdc  11160  clim  12063  dvdsaddre2b  12624  pceu  13094  divsfval  13698  sgrppropd  13777  mndpropd  13802  issubg3  14044  resghm2b  14114  rngpropd  14303  dvdsrd  14450  opprsubrngg  14568  subrngpropd  14573  subrgpropd  14610  rhmpropd  14611  lmodprop2d  14734  assapropd  15063  cnrest2  15386  cnptoprest2  15390  lmss  15396  reopnap  15696  limcdifap  15812  iswlkg  16668  isclwwlkng  16745