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 3437 nn0eln0 4602 nntri3 6474 fin0 6861 omp1eomlem 7069 ctssdccl 7086 ismkvnex 7129 xrlttri3 9747 nltpnft 9764 ngtmnft 9767 xrrebnd 9769 xltadd1 9826 xposdif 9832 xleaddadd 9837 hashnncl 10723 zfz1isolemiso 10767 mod2eq1n2dvds 11831 m1exp1 11853 pceq0 12268 |
Copyright terms: Public domain | W3C validator |