|   | 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 3868 ab0w 4378 csbprc 4408 ralf0 4513 ordsssuc2 6474 ndmovord 7624 ordsucelsuc 7843 brdomg 8998 brdomgOLD 8999 suppeqfsuppbi 9420 funsnfsupp 9433 r1pw 9886 r1pwALT 9887 elixx3g 13401 elfz2 13555 bifald 38095 areaquad 43233 | 
| Copyright terms: Public domain | W3C validator |