Theorem pm5.21nd 800

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  5773  fvelimab  6873  brrpssg  7610  ordsucelsuc  7701  releldm2  7916  relbrtpos  8084  relelec  8574  elfiun  9233  fpwwe2lem2  10434  fpwwelem  10447  fzrev3  13368  elfzp12  13381  eqgval  18850  eltg  22152  eltg2  22153  cncnp2  22477  isref  22705  islocfin  22713  opeldifid  30983  isfne  34573  copsex2b  35355  bj-ideqgALT  35373  bj-idreseq  35377  bj-ideqg1ALT  35380  opelopab3  35919  isdivrngo  36152  brssr  36661  islshpkrN  37176  dihatexv2  39395