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  3067  rmob  3082  epelg  4326  eqbrrdva  4837  elrelimasn  5036  relbrcnvg  5049  fmptco  5731  ovelrn  6076  brtpos2  6318  elpmg  6732  brdomg  6816  elfi2  7047  genpelvl  7598  genpelvu  7599  fzoval  10242  nninfinf  10554  clim  11465  dvdsaddre2b  12025  pceu  12491  divsfval  13032  sgrppropd  13117  mndpropd  13144  issubg3  13400  resghm2b  13470  rngpropd  13589  dvdsrd  13728  opprsubrngg  13845  subrngpropd  13850  subrgpropd  13887  rhmpropd  13888  lmodprop2d  13982  cnrest2  14558  cnptoprest2  14562  lmss  14568  reopnap  14868  limcdifap  14984