Theorem 2falsed 704

Description: Two falsehoods are equivalent (deduction form). (Contributed by NM, 11-Oct-2013.)

Hypotheses

Ref	Expression
2falsed.1	⊢ (𝜑 → ¬ 𝜓)
2falsed.2	⊢ (𝜑 → ¬ 𝜒)

Assertion

Ref	Expression
2falsed	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Proof of Theorem 2falsed

Step	Hyp	Ref	Expression
1		2falsed.1	. . 3 ⊢ (𝜑 → ¬ 𝜓)
2	1	pm2.21d 620	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		2falsed.2	. . 3 ⊢ (𝜑 → ¬ 𝜒)
4	3	pm2.21d 620	. 2 ⊢ (𝜑 → (𝜒 → 𝜓))
5	2, 4	impbid 129	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108  ax-in2 616

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm5.21ni  705  bianfd  951  abvor0dc  3486  nn0eln0  4673  nntri3  6593  fin0  6994  omp1eomlem  7208  ctssdccl  7225  ismkvnex  7269  xrlttri3  9932  nltpnft  9949  ngtmnft  9952  xrrebnd  9954  xltadd1  10011  xposdif  10017  xleaddadd  10022  xqltnle  10423  hashnncl  10953  zfz1isolemiso  10997  mod2eq1n2dvds  12240  m1exp1  12262  bitsmod  12317  pceq0  12695  2omap  16047