Theorem pm5.21nd 814

Description: Eliminate an antecedent implied by each side of a biconditional. Variant of pm5.21ndd 382. (Contributed by NM, 20-Nov-2005.) (Proof shortened by Wolf Lammen, 4-Nov-2013.)

Hypotheses

Ref	Expression
pm5.21nd.1	⊢ ((𝜑 ∧ 𝜓) → 𝜃)
pm5.21nd.2	⊢ ((𝜑 ∧ 𝜒) → 𝜃)
pm5.21nd.3	⊢ (𝜃 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
pm5.21nd	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Proof of Theorem pm5.21nd

Step	Hyp	Ref	Expression
1		pm5.21nd.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
2	1	ex 418	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
3		pm5.21nd.2	. . 3 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
4	3	ex 418	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
5		pm5.21nd.3	. . 3 ⊢ (𝜃 → (𝜓 ↔ 𝜒))
6	5	a1i 11	. 2 ⊢ (𝜑 → (𝜃 → (𝜓 ↔ 𝜒)))
7	2, 4, 6	pm5.21ndd 382	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ideqg  5828  fvelimab  6957  brrpssg  7741  ordsucelsuc  7833  releldm2  8054  relbrtpos  8257  relelec  8768  elfiun  9425  fpwwe2lem2  10720  fpwwelem  10733  fzrev3  13727  elfzp12  13740  eqgval  19394  ismhp  22466  eltg  23280  eltg2  23281  cncnp2  23604  isref  23833  islocfin  23841  opeldifid  33240  isfne  37219  copsex2b  38154  bj-ideqgALT  38172  bj-idreseq  38176  bj-ideqg1ALT  38179  opelopab3  38745  isdivrngo  38977  brssr  39606  islshpkrN  40270  dihatexv2  42489  isinito4a  50779  cmddu  50944