Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 2falsed | Unicode 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 614 | . 2 |
3 | 2falsed.2 | . . 3 | |
4 | 3 | pm2.21d 614 | . 2 |
5 | 2, 4 | impbid 128 | 1 |
Colors of variables: wff set class |
Syntax hints: wn 3 wi 4 wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia2 106 ax-ia3 107 ax-in2 610 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: pm5.21ni 698 bianfd 943 abvor0dc 3438 nn0eln0 4604 nntri3 6476 fin0 6863 omp1eomlem 7071 ctssdccl 7088 ismkvnex 7131 xrlttri3 9754 nltpnft 9771 ngtmnft 9774 xrrebnd 9776 xltadd1 9833 xposdif 9839 xleaddadd 9844 hashnncl 10730 zfz1isolemiso 10774 mod2eq1n2dvds 11838 m1exp1 11860 pceq0 12275 |
Copyright terms: Public domain | W3C validator |