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  5829  fvelimab  6949  brrpssg  7730  ordsucelsuc  7822  releldm2  8043  relbrtpos  8238  relelec  8749  elfiun  9406  fpwwe2lem2  10698  fpwwelem  10711  fzrev3  13704  elfzp12  13717  eqgval  19369  ismhp  22441  eltg  23255  eltg2  23256  cncnp2  23579  isref  23808  islocfin  23816  opeldifid  33175  isfne  37097  copsex2b  38029  bj-ideqgALT  38047  bj-idreseq  38051  bj-ideqg1ALT  38054  opelopab3  38620  isdivrngo  38852  brssr  39481  islshpkrN  40145  dihatexv2  42364  isinito4a  50600  cmddu  50720