Theorem 2falsed 697

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm5.21ni  698  bianfd  943  abvor0dc  3438  nn0eln0  4604  nntri3  6476  fin0  6863  omp1eomlem  7071  ctssdccl  7088  ismkvnex  7131  xrlttri3  9754  nltpnft  9771  ngtmnft  9774  xrrebnd  9776  xltadd1  9833  xposdif  9839  xleaddadd  9844  hashnncl  10730  zfz1isolemiso  10774  mod2eq1n2dvds  11838  m1exp1  11860  pceq0  12275