Theorem pm5.21ni 382

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 157	. 2 ⊢ (¬ 𝜓 → ¬ 𝜑)
3		pm5.21ni.2	. . 3 ⊢ (𝜒 → 𝜓)
4	3	con3i 157	. 2 ⊢ (¬ 𝜓 → ¬ 𝜒)
5	2, 4	2falsed 380	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  383  norbi  887  pm5.54  1018  niabn  1021  ab0w  4274  csbprc  4307  ralf0  4411  ordsssuc2  6279  ndmovord  7376  ordsucelsuc  7579  brdomg  8616  suppeqfsuppbi  8977  funsnfsupp  8987  r1pw  9426  r1pwALT  9427  elixx3g  12913  elfz2  13067  bifald  35931  areaquad  40691