Theorem pm5.21ndd 706

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 178	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
5		pm5.21ndd.2	. . . . 5 ⊢ (𝜑 → (𝜃 → 𝜓))
6	5, 2	syld 45	. . . 4 ⊢ (𝜑 → (𝜃 → (𝜒 ↔ 𝜃)))
7		bicom1 131	. . . 4 ⊢ ((𝜒 ↔ 𝜃) → (𝜃 ↔ 𝜒))
8	6, 7	syl6 33	. . 3 ⊢ (𝜑 → (𝜃 → (𝜃 ↔ 𝜒)))
9	8	ibd 178	. 2 ⊢ (𝜑 → (𝜃 → 𝜒))
10	4, 9	impbid 129	1 ⊢ (𝜑 → (𝜒 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm5.21nd  917  sbcrext  3064  rmob  3079  epelg  4322  eqbrrdva  4833  elrelimasn  5032  relbrcnvg  5045  fmptco  5725  ovelrn  6069  brtpos2  6306  elpmg  6720  brdomg  6804  elfi2  7033  genpelvl  7574  genpelvu  7575  fzoval  10217  nninfinf  10517  clim  11427  dvdsaddre2b  11987  pceu  12436  divsfval  12914  sgrppropd  12999  mndpropd  13024  issubg3  13265  resghm2b  13335  rngpropd  13454  dvdsrd  13593  opprsubrngg  13710  subrngpropd  13715  subrgpropd  13752  rhmpropd  13753  lmodprop2d  13847  cnrest2  14415  cnptoprest2  14419  lmss  14425  reopnap  14725  limcdifap  14841