Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 2falsed | Structured version Visualization version Unicode version |
Description: Two falsehoods are equivalent (deduction rule). (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 118 | . 2 |
3 | 2falsed.2 | . . 3 | |
4 | 3 | pm2.21d 118 | . 2 |
5 | 2, 4 | impbid 202 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wn 3 wi 4 wb 196 |
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 197 |
This theorem is referenced by: pm5.21ni 367 bianfd 967 sbcrextOLD 3512 sbcel12 3983 sbcne12 3986 sbcel2 3989 sbcbr 4707 csbxp 5200 smoord 7462 tfr2b 7492 axrepnd 9416 hasheq0 13154 m1exp1 15093 sadcadd 15180 stdbdxmet 22320 iccpnfcnv 22743 cxple2 24443 mirbtwnhl 25575 uvtxa01vtx 26298 eupth2lem1 27078 isoun 29479 1smat1 29870 xrge0iifcnv 29979 sgn0bi 30609 signswch 30638 fz0n 31616 hfext 32290 unccur 33392 ntrneiel2 38384 ntrneik4w 38398 eliin2f 39287 |
Copyright terms: Public domain | W3C validator |