![]() |
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 265 | . 2 ⊢ (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒)) |
4 | 3 | con4bid 317 | 1 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 |
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 206 |
This theorem is referenced by: pm5.21ni 379 bianfd 536 sbcel12 4369 sbcne12 4373 sbcel2 4376 sbcbr 5161 csbxp 5732 smoord 8312 tfr2b 8343 axrepnd 10531 hasheq0 14264 m1exp1 16259 sadcadd 16339 stdbdxmet 23874 iccpnfcnv 24310 cxple2 26055 mirbtwnhl 27625 eupth2lem1 29165 isoun 31618 1smat1 32388 xrge0iifcnv 32517 sgn0bi 33150 signswch 33176 fmlafvel 33982 fz0n 34306 hfext 34771 unccur 36064 ntrneiel2 42365 ntrneik4w 42379 eliin2f 43321 |
Copyright terms: Public domain | W3C validator |