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  3531  nn0eln0  4741  nntri3  6729  fin0  7141  2omap  7268  omp1eomlem  7384  ctssdccl  7401  ismkvnex  7445  xrlttri3  10129  nltpnft  10146  ngtmnft  10149  xrrebnd  10151  xltadd1  10208  xposdif  10214  xleaddadd  10219  xqltnle  10626  hashnncl  11156  zfz1isolemiso  11207  mod2eq1n2dvds  12561  m1exp1  12583  bitsmod  12638  pceq0  13016