Theorem 2falsed 707

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm5.21ni  708  bianfd  954  abvor0dc  3515  nn0eln0  4712  nntri3  6651  fin0  7055  omp1eomlem  7269  ctssdccl  7286  ismkvnex  7330  xrlttri3  10001  nltpnft  10018  ngtmnft  10021  xrrebnd  10023  xltadd1  10080  xposdif  10086  xleaddadd  10091  xqltnle  10495  hashnncl  11025  zfz1isolemiso  11069  mod2eq1n2dvds  12398  m1exp1  12420  bitsmod  12475  pceq0  12853  2omap  16388