Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > pm5.21ni | Structured version Visualization version GIF version |
Description: Two propositions implying a false one are equivalent. (Contributed by NM, 16-Feb-1996.) (Proof shortened by Wolf Lammen, 19-May-2013.) |
Ref | Expression |
---|---|
pm5.21ni.1 | ⊢ (𝜑 → 𝜓) |
pm5.21ni.2 | ⊢ (𝜒 → 𝜓) |
Ref | Expression |
---|---|
pm5.21ni | ⊢ (¬ 𝜓 → (𝜑 ↔ 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm5.21ni.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | 1 | con3i 157 | . 2 ⊢ (¬ 𝜓 → ¬ 𝜑) |
3 | pm5.21ni.2 | . . 3 ⊢ (𝜒 → 𝜓) | |
4 | 3 | con3i 157 | . 2 ⊢ (¬ 𝜓 → ¬ 𝜒) |
5 | 2, 4 | 2falsed 380 | 1 ⊢ (¬ 𝜓 → (𝜑 ↔ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 |
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 210 |
This theorem is referenced by: pm5.21nii 383 norbi 887 pm5.54 1018 niabn 1021 ab0w 4274 csbprc 4307 ralf0 4411 ordsssuc2 6279 ndmovord 7376 ordsucelsuc 7579 brdomg 8616 suppeqfsuppbi 8977 funsnfsupp 8987 r1pw 9426 r1pwALT 9427 elixx3g 12913 elfz2 13067 bifald 35931 areaquad 40691 |
Copyright terms: Public domain | W3C validator |