Theorem 2falsed 714

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 628	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		2falsed.2	. . 3 ⊢ (𝜑 → ¬ 𝜒)
4	3	pm2.21d 628	. 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 624

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm5.21ni  715  bianfd  961  abvor0dc  3545  nn0eln0  4765  nntri3  6764  fin0  7183  2omap  7312  omp1eomlem  7428  ctssdccl  7445  ismkvnex  7489  xrlttri3  10182  nltpnft  10199  ngtmnft  10202  xrrebnd  10204  xltadd1  10261  xposdif  10267  xleaddadd  10272  xqltnle  10685  hashnncl  11217  zfz1isolemiso  11274  mod2eq1n2dvds  12629  m1exp1  12651  bitsmod  12706  pceq0  13084