Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 2thd | GIF 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 8702 xrlttri3 9538 nltpnft 9552 ngtmnft 9555 xrrebnd 9557 xltadd1 9614 xsubge0 9619 xposdif 9620 xlesubadd 9621 xleaddadd 9625 iccshftr 9732 iccshftl 9734 iccdil 9736 icccntr 9738 fzaddel 9794 elfzomelpfzo 9963 nnesq 10366 hashnncl 10497 zfz1isolemiso 10537 mod2eq1n2dvds 11488 m1exp1 11510 dfgcd3 11610 dvdssq 11631 lmss 12326 lmres 12328 |
Copyright terms: Public domain | W3C validator |