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  3520  nn0eln0  4724  nntri3  6708  fin0  7117  omp1eomlem  7336  ctssdccl  7353  ismkvnex  7397  xrlttri3  10075  nltpnft  10092  ngtmnft  10095  xrrebnd  10097  xltadd1  10154  xposdif  10160  xleaddadd  10165  xqltnle  10571  hashnncl  11101  zfz1isolemiso  11147  mod2eq1n2dvds  12501  m1exp1  12523  bitsmod  12578  pceq0  12956  2omap  16695