Theorem pm5.21nd 801

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  ideqg  5815  fvelimab  6933  brrpssg  7701  ordsucelsuc  7797  releldm2  8022  relbrtpos  8216  relelec  8718  elfiun  9381  fpwwe2lem2  10585  fpwwelem  10598  fzrev3  13551  elfzp12  13564  eqgval  19109  ismhp  22027  eltg  22844  eltg2  22845  cncnp2  23168  isref  23396  islocfin  23404  opeldifid  32528  isfne  36327  copsex2b  37128  bj-ideqgALT  37146  bj-idreseq  37150  bj-ideqg1ALT  37153  opelopab3  37712  isdivrngo  37944  brssr  38492  islshpkrN  39113  dihatexv2  41333  isinito4a  49537  cmddu  49657