Theorem pm5.21nd 800

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 399

This theorem is referenced by:  ideqg  5724  fvelimab  6739  brrpssg  7453  ordsucelsuc  7539  releldm2  7744  relbrtpos  7905  relelec  8336  elfiun  8896  fpwwe2lem2  10056  fpwwelem  10069  fzrev3  12976  elfzp12  12989  eqgval  18331  eltg  21567  eltg2  21568  cncnp2  21891  isref  22119  islocfin  22127  opeldifid  30351  isfne  33689  copsex2b  34434  bj-ideqgALT  34452  bj-idreseq  34456  bj-ideqg1ALT  34459  opelopab3  34994  isdivrngo  35230  brssr  35743  islshpkrN  36258  dihatexv2  38477