Theorem 2falsed 707

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm5.21ni  708  bianfd  954  abvor0dc  3516  nn0eln0  4716  nntri3  6660  fin0  7069  omp1eomlem  7287  ctssdccl  7304  ismkvnex  7348  xrlttri3  10025  nltpnft  10042  ngtmnft  10045  xrrebnd  10047  xltadd1  10104  xposdif  10110  xleaddadd  10115  xqltnle  10520  hashnncl  11050  zfz1isolemiso  11096  mod2eq1n2dvds  12433  m1exp1  12455  bitsmod  12510  pceq0  12888  2omap  16544