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 172 | . 2 | |
4 | 1, 2, 3 | sylc 62 | 1 |
Colors of variables: wff set class |
Syntax hints: 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 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: rspcime 2770 abvor0dc 3356 exmidsssn 4095 euotd 4146 nn0eln0 4503 elabrex 5627 riota5f 5722 nntri3 6361 fin0 6747 omp1eomlem 6947 ctssdccl 6964 ismkvnex 6997 nn1m1nn 8706 xrlttri3 9551 nltpnft 9565 ngtmnft 9568 xrrebnd 9570 xltadd1 9627 xsubge0 9632 xposdif 9633 xlesubadd 9634 xleaddadd 9638 iccshftr 9745 iccshftl 9747 iccdil 9749 icccntr 9751 fzaddel 9807 elfzomelpfzo 9976 nnesq 10379 hashnncl 10510 zfz1isolemiso 10550 mod2eq1n2dvds 11503 m1exp1 11525 dfgcd3 11625 dvdssq 11646 lmss 12342 lmres 12344 |
Copyright terms: Public domain | W3C validator |