Theorem pm5.21nd 802

Description: Eliminate an antecedent implied by each side of a biconditional. Variant of pm5.21ndd 379. (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 412	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
3		pm5.21nd.2	. . 3 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
4	3	ex 412	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
5		pm5.21nd.3	. . 3 ⊢ (𝜃 → (𝜓 ↔ 𝜒))
6	5	a1i 11	. 2 ⊢ (𝜑 → (𝜃 → (𝜓 ↔ 𝜒)))
7	2, 4, 6	pm5.21ndd 379	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  ideqg  5800  fvelimab  6906  brrpssg  7672  ordsucelsuc  7766  releldm2  7989  relbrtpos  8180  relelec  8684  elfiun  9336  fpwwe2lem2  10546  fpwwelem  10559  fzrev3  13535  elfzp12  13548  eqgval  19143  ismhp  22116  eltg  22932  eltg2  22933  cncnp2  23256  isref  23484  islocfin  23492  opeldifid  32684  isfne  36537  copsex2b  37470  bj-ideqgALT  37488  bj-idreseq  37492  bj-ideqg1ALT  37495  opelopab3  38053  isdivrngo  38285  brssr  38916  islshpkrN  39580  dihatexv2  41799  isinito4a  50035  cmddu  50155