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  5808  fvelimab  6914  brrpssg  7680  ordsucelsuc  7774  releldm2  7997  relbrtpos  8189  relelec  8693  elfiun  9345  fpwwe2lem2  10555  fpwwelem  10568  fzrev3  13518  elfzp12  13531  eqgval  19118  ismhp  22095  eltg  22913  eltg2  22914  cncnp2  23237  isref  23465  islocfin  23473  opeldifid  32685  isfne  36552  copsex2b  37389  bj-ideqgALT  37407  bj-idreseq  37411  bj-ideqg1ALT  37414  opelopab3  37963  isdivrngo  38195  brssr  38826  islshpkrN  39490  dihatexv2  41709  isinito4a  49901  cmddu  50021