![]() |
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 378 bianfd 535 sbcel12 4408 sbcne12 4412 sbcel2 4415 sbcbr 5203 csbxp 5775 smoord 8367 tfr2b 8398 axrepnd 10591 hasheq0 14327 m1exp1 16323 sadcadd 16403 stdbdxmet 24244 iccpnfcnv 24684 cxple2 26429 mirbtwnhl 28186 eupth2lem1 29726 ifnebib 32036 isoun 32178 1smat1 33070 xrge0iifcnv 33199 sgn0bi 33832 signswch 33858 fmlafvel 34662 fz0n 34992 hfext 35447 unccur 36774 ntrneiel2 43139 ntrneik4w 43153 eliin2f 44095 |
Copyright terms: Public domain | W3C validator |