Theorem pm5.21ndd 707

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  918  sbcrext  3077  rmob  3092  epelg  4341  eqbrrdva  4852  elrelimasn  5053  relbrcnvg  5066  fmptco  5753  ovelrn  6102  brtpos2  6344  elpmg  6758  brdomg  6844  elfi2  7081  genpelvl  7632  genpelvu  7633  fzoval  10277  nninfinf  10595  clim  11636  dvdsaddre2b  12196  pceu  12662  divsfval  13204  sgrppropd  13289  mndpropd  13316  issubg3  13572  resghm2b  13642  rngpropd  13761  dvdsrd  13900  opprsubrngg  14017  subrngpropd  14022  subrgpropd  14059  rhmpropd  14060  lmodprop2d  14154  cnrest2  14752  cnptoprest2  14756  lmss  14762  reopnap  15062  limcdifap  15178