Theorem pm5.21nd 801

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

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

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 398

This theorem is referenced by:  ideqg  5852  fvelimab  6965  brrpssg  7715  ordsucelsuc  7810  releldm2  8029  relbrtpos  8222  relelec  8748  elfiun  9425  fpwwe2lem2  10627  fpwwelem  10640  fzrev3  13567  elfzp12  13580  eqgval  19057  eltg  22460  eltg2  22461  cncnp2  22785  isref  23013  islocfin  23021  opeldifid  31830  isfne  35224  copsex2b  36021  bj-ideqgALT  36039  bj-idreseq  36043  bj-ideqg1ALT  36046  opelopab3  36586  isdivrngo  36818  brssr  37371  islshpkrN  37990  dihatexv2  40210