Theorem pm5.21ni 367

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 150	. 2 ⊢ (¬ 𝜓 → ¬ 𝜑)
3		pm5.21ni.2	. . 3 ⊢ (𝜒 → 𝜓)
4	3	con3i 150	. 2 ⊢ (¬ 𝜓 → ¬ 𝜒)
5	2, 4	2falsed 366	1 ⊢ (¬ 𝜓 → (𝜑 ↔ 𝜒))

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

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 197

This theorem is referenced by:  pm5.21nii  368  norbi  904  pm5.54  943  niabn  964  csbprc  3980  ordsssuc2  5814  ndmovord  6824  ordsucelsuc  7022  brdomg  7965  suppeqfsuppbi  8289  funsnfsupp  8299  r1pw  8708  r1pwALT  8709  elixx3g  12188  elfz2  12333  bifald  33888  areaquad  37802