Theorem pm5.21nd 814

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ideqg  5835  fvelimab  6980  brrpssg  7765  ordsucelsuc  7857  releldm2  8078  relbrtpos  8282  relelec  8793  elfiun  9449  fpwwe2lem2  10744  fpwwelem  10757  fzrev3  13751  elfzp12  13764  eqgval  19418  ismhp  22491  eltg  23305  eltg2  23306  cncnp2  23629  isref  23858  islocfin  23866  opeldifid  33265  isfne  37305  copsex2b  38253  bj-ideqgALT  38271  bj-idreseq  38275  bj-ideqg1ALT  38278  opelopab3  38844  isdivrngo  39076  brssr  39705  islshpkrN  40369  dihatexv2  42588  isinito4a  50891  cmddu  51056