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 378 | 1 ⊢ (¬ 𝜓 → (𝜑 ↔ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 |
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 208 |
This theorem is referenced by: pm5.21nii 380 norbi 880 pm5.54 1011 niabn 1014 csbprc 4355 ordsssuc2 6272 ndmovord 7327 ordsucelsuc 7526 brdomg 8507 suppeqfsuppbi 8835 funsnfsupp 8845 r1pw 9262 r1pwALT 9263 elixx3g 12739 elfz2 12887 bifald 35246 areaquad 39701 |
Copyright terms: Public domain | W3C validator |