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  5722  fvelimab  6737  brrpssg  7451  ordsucelsuc  7537  releldm2  7742  relbrtpos  7903  relelec  8334  elfiun  8894  fpwwe2lem2  10054  fpwwelem  10067  fzrev3  12974  elfzp12  12987  eqgval  18329  eltg  21565  eltg2  21566  cncnp2  21889  isref  22117  islocfin  22125  opeldifid  30349  isfne  33687  copsex2b  34435  bj-ideqgALT  34453  bj-idreseq  34457  bj-ideqg1ALT  34460  opelopab3  35007  isdivrngo  35243  brssr  35756  islshpkrN  36271  dihatexv2  38490