Theorem 2falsed 659

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 589	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		2falsed.2	. . 3 ⊢ (𝜑 → ¬ 𝜒)
4	3	pm2.21d 589	. 2 ⊢ (𝜑 → (𝜒 → 𝜓))
5	2, 4	impbid 128	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 106  ax-ia3 107  ax-in2 585

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm5.21ni  660  bianfd  900  abvor0dc  3333  nn0eln0  4471  nntri3  6323  fin0  6708  omp1eomlem  6894  ctssdclemr  6911  xrlttri3  9424  nltpnft  9438  ngtmnft  9441  xrrebnd  9443  xltadd1  9500  xposdif  9506  xleaddadd  9511  hashnncl  10383  zfz1isolemiso  10423  mod2eq1n2dvds  11371  m1exp1  11393