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  3821  csbprc  4370  ordsssuc2  6482  ndmovord  7643  ordsucelsuc  7867  brdomg  9023  suppeqfsuppbi  9408  funsnfsupp  9421  r1pw  9896  r1pwALT  9897  elixx3g  13529  elfz2  13686  bifald  39287  quadfac  43521  areaquad  44479