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  9891  nltpnft  9908  ngtmnft  9911  xrrebnd  9913  xltadd1  9970  xposdif  9976  xleaddadd  9981  xqltnle  10376  hashnncl  10906  zfz1isolemiso  10950  mod2eq1n2dvds  12063  m1exp1  12085  bitsmod  12140  pceq0  12518  2omap  15750