Theorem pm5.21nd 800

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  ideqg  5851  fvelimab  6964  brrpssg  7717  ordsucelsuc  7812  releldm2  8031  relbrtpos  8224  relelec  8750  elfiun  9427  fpwwe2lem2  10629  fpwwelem  10642  fzrev3  13569  elfzp12  13582  eqgval  19059  eltg  22467  eltg2  22468  cncnp2  22792  isref  23020  islocfin  23028  opeldifid  31868  isfne  35310  copsex2b  36107  bj-ideqgALT  36125  bj-idreseq  36129  bj-ideqg1ALT  36132  opelopab3  36672  isdivrngo  36904  brssr  37457  islshpkrN  38076  dihatexv2  40296