Theorem pm5.21nd 811

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 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 381	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 208   ∧ 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 209  df-an 400

This theorem is referenced by:  ideqg  5821  fvelimab  6935  brrpssg  7704  ordsucelsuc  7798  releldm2  8020  relbrtpos  8212  relelec  8721  elfiun  9373  fpwwe2lem2  10587  fpwwelem  10600  fzrev3  13592  elfzp12  13605  eqgval  19201  ismhp  22185  eltg  22997  eltg2  22998  cncnp2  23321  isref  23549  islocfin  23557  opeldifid  32748  isfne  36663  copsex2b  37596  bj-ideqgALT  37614  bj-idreseq  37618  bj-ideqg1ALT  37621  opelopab3  38181  isdivrngo  38413  brssr  39044  islshpkrN  39708  dihatexv2  41927  isinito4a  50133  cmddu  50253