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  6455  ndmovord  7609  ordsucelsuc  7831  brdomg  8978  suppeqfsuppbi  9364  funsnfsupp  9377  r1pw  9852  r1pwALT  9853  elixx3g  13482  elfz2  13639  bifald  39001  quadfac  43235  areaquad  44202