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 2800 abvor0dc 3391 exmidsssn 4133 euotd 4184 nn0eln0 4541 elabrex 5667 riota5f 5762 nntri3 6401 fin0 6787 omp1eomlem 6987 ctssdccl 7004 ismkvnex 7037 nn1m1nn 8762 xrlttri3 9613 nltpnft 9627 ngtmnft 9630 xrrebnd 9632 xltadd1 9689 xsubge0 9694 xposdif 9695 xlesubadd 9696 xleaddadd 9700 iccshftr 9807 iccshftl 9809 iccdil 9811 icccntr 9813 fzaddel 9870 elfzomelpfzo 10039 nnesq 10442 hashnncl 10574 zfz1isolemiso 10614 mod2eq1n2dvds 11612 m1exp1 11634 dfgcd3 11734 dvdssq 11755 lmss 12454 lmres 12456 |
Copyright terms: Public domain | W3C validator |