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  5806  fvelimab  6912  brrpssg  7679  ordsucelsuc  7773  releldm2  7996  relbrtpos  8187  relelec  8691  elfiun  9343  fpwwe2lem2  10555  fpwwelem  10568  fzrev3  13544  elfzp12  13557  eqgval  19152  ismhp  22106  eltg  22922  eltg2  22923  cncnp2  23246  isref  23474  islocfin  23482  opeldifid  32669  isfne  36521  copsex2b  37454  bj-ideqgALT  37472  bj-idreseq  37476  bj-ideqg1ALT  37479  opelopab3  38039  isdivrngo  38271  brssr  38902  islshpkrN  39566  dihatexv2  41785  isinito4a  50023  cmddu  50143