![]() |
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 264 | . 2 ⊢ (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒)) |
4 | 3 | con4bid 316 | 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 376 bianfd 533 sbcel12 4410 sbcne12 4414 sbcel2 4417 sbcbr 5205 csbxp 5779 smoord 8390 tfr2b 8421 axrepnd 10623 hasheq0 14360 m1exp1 16358 sadcadd 16438 stdbdxmet 24442 iccpnfcnv 24887 cxple2 26649 mirbtwnhl 28502 eupth2lem1 30046 ifnebib 32358 isoun 32499 1smat1 33410 xrge0iifcnv 33539 sgn0bi 34172 signswch 34198 fmlafvel 35000 fz0n 35330 hfext 35784 unccur 37081 ntrneiel2 43519 ntrneik4w 43533 eliin2f 44473 |
Copyright terms: Public domain | W3C validator |