![]() |
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.) |
Ref | Expression |
---|---|
2falsed.1 | ⊢ (𝜑 → ¬ 𝜓) |
2falsed.2 | ⊢ (𝜑 → ¬ 𝜒) |
Ref | Expression |
---|---|
2falsed | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2falsed.1 | . . 3 ⊢ (𝜑 → ¬ 𝜓) | |
2 | 1 | pm2.21d 121 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) |
3 | 2falsed.2 | . . 3 ⊢ (𝜑 → ¬ 𝜒) | |
4 | 3 | pm2.21d 121 | . 2 ⊢ (𝜑 → (𝜒 → 𝜓)) |
5 | 2, 4 | impbid 213 | 1 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 |
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 208 |
This theorem is referenced by: pm5.21ni 379 bianfd 535 sbcel12 4284 sbcne12 4288 sbcel2 4291 sbcbr 5021 csbxp 5541 smoord 7859 tfr2b 7889 axrepnd 9867 hasheq0 13579 m1exp1 15565 sadcadd 15645 stdbdxmet 22813 iccpnfcnv 23236 cxple2 24966 mirbtwnhl 26153 eupth2lem1 27690 isoun 30130 1smat1 30689 xrge0iifcnv 30798 sgn0bi 31427 signswch 31453 fmlafvel 32247 fz0n 32577 hfext 33260 unccur 34432 ntrneiel2 39947 ntrneik4w 39961 eliin2f 40936 |
Copyright terms: Public domain | W3C validator |