Theorem 2falsed 710

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  711  bianfd  957  abvor0dc  3536  nn0eln0  4747  nntri3  6743  fin0  7155  2omap  7282  omp1eomlem  7398  ctssdccl  7415  ismkvnex  7459  xrlttri3  10149  nltpnft  10166  ngtmnft  10169  xrrebnd  10171  xltadd1  10228  xposdif  10234  xleaddadd  10239  xqltnle  10651  hashnncl  11183  zfz1isolemiso  11236  mod2eq1n2dvds  12590  m1exp1  12612  bitsmod  12667  pceq0  13045