Theorem pm5.21nd 813

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 417	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
3		pm5.21nd.2	. . 3 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
4	3	ex 417	. 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 400

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 401

This theorem is used by:  ideqg  5837  fvelimab  6953  brrpssg  7722  ordsucelsuc  7814  releldm2  8036  relbrtpos  8229  relelec  8738  elfiun  9386  fpwwe2lem2  10621  fpwwelem  10634  fzrev3  13623  elfzp12  13636  eqgval  19249  ismhp  22312  eltg  23123  eltg2  23124  cncnp2  23447  isref  23675  islocfin  23683  opeldifid  32953  isfne  36878  copsex2b  37812  bj-ideqgALT  37830  bj-idreseq  37834  bj-ideqg1ALT  37837  opelopab3  38397  isdivrngo  38629  brssr  39258  islshpkrN  39922  dihatexv2  42141  isinito4a  50354  cmddu  50474