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  3817  csbprc  4367  ordsssuc2  6451  ndmovord  7604  ordsucelsuc  7818  brdomg  8964  suppeqfsuppbi  9349  funsnfsupp  9362  r1pw  9827  r1pwALT  9828  elixx3g  13411  elfz2  13568  bifald  38837  quadfac  43071  areaquad  44057