Theorem pm5.21ni 366

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

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

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 196

This theorem is referenced by:  pm5.21nii  367  norbi  900  pm5.54  941  niabn  989  csbprc  3932  ordsssuc2  5731  ndmovord  6722  ordsucelsuc  6914  brdomg  7851  suppeqfsuppbi  8172  funsnfsupp  8182  r1pw  8591  r1pwALT  8592  elixx3g  12059  elfz2  12204  bifald  33058  areaquad  36821