Theorem pm5.21nd 807

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  ideqg  5800  fvelimab  6906  brrpssg  7675  ordsucelsuc  7769  releldm2  7992  relbrtpos  8184  relelec  8688  elfiun  9340  fpwwe2lem2  10553  fpwwelem  10566  fzrev3  13542  elfzp12  13555  eqgval  19150  ismhp  22135  eltg  22947  eltg2  22948  cncnp2  23271  isref  23499  islocfin  23507  opeldifid  32695  isfne  36574  copsex2b  37507  bj-ideqgALT  37525  bj-idreseq  37529  bj-ideqg1ALT  37532  opelopab3  38092  isdivrngo  38324  brssr  38955  islshpkrN  39619  dihatexv2  41838  isinito4a  50045  cmddu  50165