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	⊢ (𝜑 → (𝜒 → 𝜓))
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  928  sbcrext  3129  rmob  3145  epelg  4433  eqbrrdva  4948  elrelimasn  5151  relbrcnvg  5164  fmptco  5868  ovelrn  6232  suppcofn  6500  brtpos2  6516  elpmg  6932  brdomg  7026  suppeqfsuppbi  7289  elfi2  7300  genpelvl  7873  genpelvu  7874  fzoval  10538  nninfinf  10863  clim  12030  dvdsaddre2b  12591  pceu  13057  divsfval  13632  sgrppropd  13711  mndpropd  13736  issubg3  13978  resghm2b  14048  rngpropd  14237  dvdsrd  14384  opprsubrngg  14502  subrngpropd  14507  subrgpropd  14544  rhmpropd  14545  lmodprop2d  14668  assapropd  14997  cnrest2  15320  cnptoprest2  15324  lmss  15330  reopnap  15630  limcdifap  15746  iswlkg  16553  isclwwlkng  16630