![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 2thd | Unicode version |
Description: Two truths are equivalent (deduction form). (Contributed by NM, 3-Jun-2012.) (Revised by NM, 29-Jan-2013.) |
Ref | Expression |
---|---|
2thd.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
2thd.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
2thd |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2thd.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 2thd.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | pm5.1im 173 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | sylc 62 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: biort 830 rspcime 2863 abvor0dc 3461 exmidsssn 4220 euotd 4272 nn0eln0 4637 elabrex 5779 elabrexg 5780 riota5f 5877 nntri3 6523 fin0 6914 omp1eomlem 7124 ctssdccl 7141 ismkvnex 7184 nn1m1nn 8968 xrlttri3 9829 nltpnft 9846 ngtmnft 9849 xrrebnd 9851 xltadd1 9908 xsubge0 9913 xposdif 9914 xlesubadd 9915 xleaddadd 9919 iccshftr 10026 iccshftl 10028 iccdil 10030 icccntr 10032 fzaddel 10091 elfzomelpfzo 10263 xqltnle 10300 nnesq 10674 hashnncl 10810 zfz1isolemiso 10854 mod2eq1n2dvds 11919 m1exp1 11941 dfgcd3 12046 dvdssq 12067 pcdvdsb 12355 pceq0 12357 issubg3 13148 lmss 14223 lmres 14225 |
Copyright terms: Public domain | W3C validator |