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  6954  brrpssg  7730  ordsucelsuc  7822  releldm2  8044  relbrtpos  8239  relelec  8748  elfiun  9404  fpwwe2lem2  10645  fpwwelem  10658  fzrev3  13649  elfzp12  13662  eqgval  19308  ismhp  22374  eltg  23188  eltg2  23189  cncnp2  23512  isref  23741  islocfin  23749  opeldifid  33080  isfne  36966  copsex2b  37900  bj-ideqgALT  37918  bj-idreseq  37922  bj-ideqg1ALT  37925  opelopab3  38476  isdivrngo  38708  brssr  39337  islshpkrN  40001  dihatexv2  42220  isinito4a  50482  cmddu  50602