![]() |
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 376 | 1 ⊢ (¬ 𝜓 → (𝜑 ↔ 𝜒)) |
Colors of variables: wff setvar class |
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 3878 ab0w 4385 csbprc 4415 ralf0 4520 ordsssuc2 6477 ndmovord 7623 ordsucelsuc 7842 brdomg 8996 brdomgOLD 8997 suppeqfsuppbi 9417 funsnfsupp 9430 r1pw 9883 r1pwALT 9884 elixx3g 13397 elfz2 13551 bifald 38074 areaquad 43205 |
Copyright terms: Public domain | W3C validator |