Theorem 2falsed 714

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108  ax-in2 624

This proof depends on definitions:  df-bi 117

This theorem is used by:  pm5.21ni  715  bianfd  961  abvor0dc  3545  nn0eln0  4769  nntri3  6774  fin0  7193  2omap  7324  omp1eomlem  7440  ctssdccl  7457  ismkvnex  7501  xrlttri3  10216  nltpnft  10233  ngtmnft  10236  xrrebnd  10238  xltadd1  10295  xposdif  10301  xleaddadd  10306  xqltnle  10719  flaplt  10739  hashnncl  11256  zfz1isolemiso  11313  mod2eq1n2dvds  12671  m1exp1  12693  bitsmod  12748  pceq0  13130