Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 2falsed | Structured version Visualization version GIF version |
Description: Two falsehoods are equivalent (deduction form). (Contributed by NM, 11-Oct-2013.) (Proof shortened by Wolf Lammen, 11-Apr-2024.) |
Ref | Expression |
---|---|
2falsed.1 | ⊢ (𝜑 → ¬ 𝜓) |
2falsed.2 | ⊢ (𝜑 → ¬ 𝜒) |
Ref | Expression |
---|---|
2falsed | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2falsed.1 | . . 3 ⊢ (𝜑 → ¬ 𝜓) | |
2 | 2falsed.2 | . . 3 ⊢ (𝜑 → ¬ 𝜒) | |
3 | 1, 2 | 2thd 268 | . 2 ⊢ (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒)) |
4 | 3 | con4bid 320 | 1 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 |
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 210 |
This theorem is referenced by: pm5.21ni 382 bianfd 538 sbcel12 4320 sbcne12 4324 sbcel2 4327 sbcbr 5105 csbxp 5644 smoord 8099 tfr2b 8129 axrepnd 10205 hasheq0 13927 m1exp1 15934 sadcadd 16014 stdbdxmet 23410 iccpnfcnv 23838 cxple2 25582 mirbtwnhl 26768 eupth2lem1 28298 isoun 30751 1smat1 31465 xrge0iifcnv 31594 sgn0bi 32223 signswch 32249 fmlafvel 33057 fz0n 33411 hfext 34219 unccur 35495 ntrneiel2 41371 ntrneik4w 41385 eliin2f 42325 |
Copyright terms: Public domain | W3C validator |