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: biort 819 rspcime 2832 abvor0dc 3427 exmidsssn 4175 euotd 4226 nn0eln0 4591 elabrex 5720 riota5f 5816 nntri3 6456 fin0 6842 omp1eomlem 7050 ctssdccl 7067 ismkvnex 7110 nn1m1nn 8866 xrlttri3 9724 nltpnft 9741 ngtmnft 9744 xrrebnd 9746 xltadd1 9803 xsubge0 9808 xposdif 9809 xlesubadd 9810 xleaddadd 9814 iccshftr 9921 iccshftl 9923 iccdil 9925 icccntr 9927 fzaddel 9984 elfzomelpfzo 10156 nnesq 10563 hashnncl 10698 zfz1isolemiso 10738 mod2eq1n2dvds 11801 m1exp1 11823 dfgcd3 11928 dvdssq 11949 pcdvdsb 12230 pceq0 12232 lmss 12793 lmres 12795 |
Copyright terms: Public domain | W3C validator |