Theorem 2falsed 709

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm5.21ni  710  bianfd  956  abvor0dc  3518  nn0eln0  4718  nntri3  6665  fin0  7074  omp1eomlem  7293  ctssdccl  7310  ismkvnex  7354  xrlttri3  10032  nltpnft  10049  ngtmnft  10052  xrrebnd  10054  xltadd1  10111  xposdif  10117  xleaddadd  10122  xqltnle  10528  hashnncl  11058  zfz1isolemiso  11104  mod2eq1n2dvds  12445  m1exp1  12467  bitsmod  12522  pceq0  12900  2omap  16620