Theorem pm5.21nd 802

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  ideqg  5720  fvelimab  6784  brrpssg  7513  ordsucelsuc  7601  releldm2  7814  relbrtpos  7979  relelec  8436  elfiun  9046  fpwwe2lem2  10246  fpwwelem  10259  fzrev3  13178  elfzp12  13191  eqgval  18593  eltg  21854  eltg2  21855  cncnp2  22178  isref  22406  islocfin  22414  opeldifid  30657  isfne  34265  copsex2b  35046  bj-ideqgALT  35064  bj-idreseq  35068  bj-ideqg1ALT  35071  opelopab3  35612  isdivrngo  35845  brssr  36356  islshpkrN  36871  dihatexv2  39090