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  6527  elpmg  6943  brdomg  7038  elfi2  7311  genpelvl  7885  genpelvu  7886  indval0  9306  fzoval  10571  nninfinf  10900  nn0sqdc  11167  clim  12071  dvdsaddre2b  12632  pceu  13102  divsfval  13707  sgrppropd  13786  mndpropd  13811  issubg3  14053  resghm2b  14123  cntzval  14152  resscntz  14165  rngpropd  14360  dvdsrd  14509  opprsubrngg  14627  subrngpropd  14632  subrgpropd  14669  rhmpropd  14670  lmodprop2d  14793  assapropd  15122  cnrest2  15479  cnptoprest2  15483  lmss  15489  reopnap  15789  limcdifap  15905  iswlkg  16792  isclwwlkng  16869