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: biort 815 rspcime 2823 abvor0dc 3417 exmidsssn 4163 euotd 4214 nn0eln0 4579 elabrex 5708 riota5f 5804 nntri3 6444 fin0 6830 omp1eomlem 7038 ctssdccl 7055 ismkvnex 7098 nn1m1nn 8851 xrlttri3 9704 nltpnft 9718 ngtmnft 9721 xrrebnd 9723 xltadd1 9780 xsubge0 9785 xposdif 9786 xlesubadd 9787 xleaddadd 9791 iccshftr 9898 iccshftl 9900 iccdil 9902 icccntr 9904 fzaddel 9961 elfzomelpfzo 10130 nnesq 10537 hashnncl 10670 zfz1isolemiso 10710 mod2eq1n2dvds 11769 m1exp1 11791 dfgcd3 11893 dvdssq 11914 lmss 12646 lmres 12648 |
Copyright terms: Public domain | W3C validator |