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  4767  nntri3  6770  fin0  7189  2omap  7319  omp1eomlem  7435  ctssdccl  7452  ismkvnex  7496  xrlttri3  10210  nltpnft  10227  ngtmnft  10230  xrrebnd  10232  xltadd1  10289  xposdif  10295  xleaddadd  10300  xqltnle  10713  flaplt  10733  hashnncl  11250  zfz1isolemiso  11307  mod2eq1n2dvds  12665  m1exp1  12687  bitsmod  12742  pceq0  13124