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 ⊢ (¬ 𝜓 → (𝜑 ↔ 𝜒))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  pm5.21nii  381  norbi  900  pm5.54  1035  niabn  1038  sbccomlem  3824  csbprc  4374  ordsssuc2  6458  ndmovord  7606  ordsucelsuc  7820  brdomg  8957  suppeqfsuppbi  9342  funsnfsupp  9355  r1pw  9820  r1pwALT  9821  elixx3g  13396  elfz2  13553  bifald  38771  quadfac  43005  areaquad  43976