Theorem 2falsed 702

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm5.21ni  703  bianfd  948  abvor0dc  3448  nn0eln0  4621  nntri3  6500  fin0  6887  omp1eomlem  7095  ctssdccl  7112  ismkvnex  7155  xrlttri3  9799  nltpnft  9816  ngtmnft  9819  xrrebnd  9821  xltadd1  9878  xposdif  9884  xleaddadd  9889  hashnncl  10777  zfz1isolemiso  10821  mod2eq1n2dvds  11886  m1exp1  11908  pceq0  12323