Theorem 2falsed 703

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm5.21ni  704  bianfd  950  abvor0dc  3470  nn0eln0  4652  nntri3  6550  fin0  6941  omp1eomlem  7153  ctssdccl  7170  ismkvnex  7214  xrlttri3  9863  nltpnft  9880  ngtmnft  9883  xrrebnd  9885  xltadd1  9942  xposdif  9948  xleaddadd  9953  xqltnle  10336  hashnncl  10866  zfz1isolemiso  10910  mod2eq1n2dvds  12020  m1exp1  12042  pceq0  12460