![]() |
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 154 | . 2 ⊢ (¬ 𝜓 → ¬ 𝜑) |
3 | pm5.21ni.2 | . . 3 ⊢ (𝜒 → 𝜓) | |
4 | 3 | con3i 154 | . 2 ⊢ (¬ 𝜓 → ¬ 𝜒) |
5 | 2, 4 | 2falsed 377 | 1 ⊢ (¬ 𝜓 → (𝜑 ↔ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 |
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 206 |
This theorem is referenced by: pm5.21nii 380 norbi 886 pm5.54 1017 niabn 1020 ab0w 4374 csbprc 4407 ralf0 4514 ordsssuc2 6456 ndmovord 7597 ordsucelsuc 7810 brdomg 8952 brdomgOLD 8953 suppeqfsuppbi 9377 funsnfsupp 9387 r1pw 9840 r1pwALT 9841 elixx3g 13337 elfz2 13491 bifald 36955 areaquad 41965 |
Copyright terms: Public domain | W3C validator |