Theorem pm5.21ndd 695

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	⊢ (𝜑 → (𝜒 → 𝜓))
pm5.21ndd.2	⊢ (𝜑 → (𝜃 → 𝜓))
pm5.21ndd.3	⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃)))

Assertion

Ref	Expression
pm5.21ndd	⊢ (𝜑 → (𝜒 ↔ 𝜃))

Proof of Theorem pm5.21ndd

Step	Hyp	Ref	Expression
1		pm5.21ndd.1	. . . 4 ⊢ (𝜑 → (𝜒 → 𝜓))
2		pm5.21ndd.3	. . . 4 ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃)))
3	1, 2	syld 45	. . 3 ⊢ (𝜑 → (𝜒 → (𝜒 ↔ 𝜃)))
4	3	ibd 177	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
5		pm5.21ndd.2	. . . . 5 ⊢ (𝜑 → (𝜃 → 𝜓))
6	5, 2	syld 45	. . . 4 ⊢ (𝜑 → (𝜃 → (𝜒 ↔ 𝜃)))
7		bicom1 130	. . . 4 ⊢ ((𝜒 ↔ 𝜃) → (𝜃 ↔ 𝜒))
8	6, 7	syl6 33	. . 3 ⊢ (𝜑 → (𝜃 → (𝜃 ↔ 𝜒)))
9	8	ibd 177	. 2 ⊢ (𝜑 → (𝜃 → 𝜒))
10	4, 9	impbid 128	1 ⊢ (𝜑 → (𝜒 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm5.21nd  906  sbcrext  3027  rmob  3042  epelg  4267  eqbrrdva  4773  relbrcnvg  4982  fmptco  5650  ovelrn  5986  brtpos2  6215  elpmg  6626  brdomg  6710  elfi2  6933  genpelvl  7449  genpelvu  7450  fzoval  10079  clim  11218  pceu  12223  cnrest2  12836  cnptoprest2  12840  lmss  12846  reopnap  13138  limcdifap  13231