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 ⊢ (𝜑 → (𝜒 ↔ 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  pm5.21nd  928  sbcrext  3129  rmob  3145  epelg  4437  eqbrrdva  4952  elrelimasn  5156  relbrcnvg  5169  relndmfv  5731  fmptco  5877  ovelrn  6241  suppcofn  6510  brtpos2  6526  elpmg  6942  brdomg  7037  suppeqfsuppbi  7301  elfi2  7312  genpelvl  7886  genpelvu  7887  indval0  9307  fzoval  10573  nninfinf  10902  nn0sqdc  11169  clim  12073  dvdsaddre2b  12634  pceu  13104  divsfval  13709  sgrppropd  13788  mndpropd  13813  issubg3  14055  resghm2b  14125  cntzval  14154  resscntz  14167  rngpropd  14362  dvdsrd  14511  opprsubrngg  14629  subrngpropd  14634  subrgpropd  14671  rhmpropd  14672  lmodprop2d  14795  assapropd  15124  cnrest2  15474  cnptoprest2  15478  lmss  15484  reopnap  15784  limcdifap  15900  iswlkg  16787  isclwwlkng  16864