Theorem pm5.21ni 377

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

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

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 207

This theorem is referenced by:  pm5.21nii  378  norbi  886  pm5.54  1019  niabn  1022  sbccomlem  3849  ab0w  4359  csbprc  4389  ralf0  4494  ordsssuc2  6450  ndmovord  7602  ordsucelsuc  7821  brdomg  8976  brdomgOLD  8977  suppeqfsuppbi  9396  funsnfsupp  9409  r1pw  9864  r1pwALT  9865  elixx3g  13380  elfz2  13536  bifald  38116  areaquad  43207