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 267 | . 2 ⊢ (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒)) |
4 | 3 | con4bid 319 | 1 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 |
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 209 |
This theorem is referenced by: pm5.21ni 381 bianfd 537 sbcel12 4362 sbcne12 4366 sbcel2 4369 sbcbr 5123 csbxp 5652 smoord 8004 tfr2b 8034 axrepnd 10018 hasheq0 13727 m1exp1 15729 sadcadd 15809 stdbdxmet 23127 iccpnfcnv 23550 cxple2 25282 mirbtwnhl 26468 eupth2lem1 27999 isoun 30439 1smat1 31071 xrge0iifcnv 31178 sgn0bi 31807 signswch 31833 fmlafvel 32634 fz0n 32964 hfext 33646 unccur 34877 ntrneiel2 40443 ntrneik4w 40457 eliin2f 41377 |
Copyright terms: Public domain | W3C validator |