![]() |
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 4334 csbprc 4367 ralf0 4472 ordsssuc2 6409 ndmovord 7545 ordsucelsuc 7758 brdomg 8897 brdomgOLD 8898 suppeqfsuppbi 9320 funsnfsupp 9330 r1pw 9782 r1pwALT 9783 elixx3g 13278 elfz2 13432 bifald 36549 areaquad 41553 |
Copyright terms: Public domain | W3C validator |