Theorem 2falsed 692

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 609	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		2falsed.2	. . 3 ⊢ (𝜑 → ¬ 𝜒)
4	3	pm2.21d 609	. 2 ⊢ (𝜑 → (𝜒 → 𝜓))
5	2, 4	impbid 128	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm5.21ni  693  bianfd  938  abvor0dc  3432  nn0eln0  4597  nntri3  6465  fin0  6851  omp1eomlem  7059  ctssdccl  7076  ismkvnex  7119  xrlttri3  9733  nltpnft  9750  ngtmnft  9753  xrrebnd  9755  xltadd1  9812  xposdif  9818  xleaddadd  9823  hashnncl  10709  zfz1isolemiso  10752  mod2eq1n2dvds  11816  m1exp1  11838  pceq0  12253