Theorem 2falsed 703

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  704  bianfd  950  abvor0dc  3475  nn0eln0  4657  nntri3  6564  fin0  6955  omp1eomlem  7169  ctssdccl  7186  ismkvnex  7230  xrlttri3  9889  nltpnft  9906  ngtmnft  9909  xrrebnd  9911  xltadd1  9968  xposdif  9974  xleaddadd  9979  xqltnle  10374  hashnncl  10904  zfz1isolemiso  10948  mod2eq1n2dvds  12061  m1exp1  12083  bitsmod  12138  pceq0  12516  2omap  15726