Theorem pm5.21ni 380

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

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

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 210

This theorem is referenced by:  pm5.21nii  381  norbi  899  pm5.54  1033  niabn  1036  sbccomlem  3831  csbprc  4372  ordsssuc2  6451  ndmovord  7598  ordsucelsuc  7814  brdomg  8951  suppeqfsuppbi  9335  funsnfsupp  9348  r1pw  9813  r1pwALT  9814  elixx3g  13381  elfz2  13538  bifald  38621  areaquad  43828