Theorem pm5.21ni 379

Description: Two propositions implying a false one are equivalent. (Contributed by NM, 16-Feb-1996.) (Proof shortened by Wolf Lammen, 19-May-2013.)

Hypotheses

Ref	Expression
pm5.21ni.1	⊢ (𝜑 → 𝜓)
pm5.21ni.2	⊢ (𝜒 → 𝜓)

Assertion

Ref	Expression
pm5.21ni	⊢ (¬ 𝜓 → (𝜑 ↔ 𝜒))

Proof of Theorem pm5.21ni

Step	Hyp	Ref	Expression
1		pm5.21ni.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	con3i 154	. 2 ⊢ (¬ 𝜓 → ¬ 𝜑)
3		pm5.21ni.2	. . 3 ⊢ (𝜒 → 𝜓)
4	3	con3i 154	. 2 ⊢ (¬ 𝜓 → ¬ 𝜒)
5	2, 4	2falsed 377	1 ⊢ (¬ 𝜓 → (𝜑 ↔ 𝜒))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206

This theorem is referenced by:  pm5.21nii  380  norbi  886  pm5.54  1017  niabn  1020  ab0w  4373  csbprc  4406  ralf0  4513  ordsssuc2  6453  ndmovord  7594  ordsucelsuc  7807  brdomg  8949  brdomgOLD  8950  suppeqfsuppbi  9374  funsnfsupp  9384  r1pw  9837  r1pwALT  9838  elixx3g  13334  elfz2  13488  bifald  36944  areaquad  41951