![]() |
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 173 | . 2 ⊢ (𝜓 → (𝜒 → (𝜓 ↔ 𝜒))) | |
4 | 1, 2, 3 | sylc 62 | 1 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 105 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: biort 829 rspcime 2848 abvor0dc 3446 exmidsssn 4202 euotd 4254 nn0eln0 4619 elabrex 5758 riota5f 5854 nntri3 6497 fin0 6884 omp1eomlem 7092 ctssdccl 7109 ismkvnex 7152 nn1m1nn 8935 xrlttri3 9795 nltpnft 9812 ngtmnft 9815 xrrebnd 9817 xltadd1 9874 xsubge0 9879 xposdif 9880 xlesubadd 9881 xleaddadd 9885 iccshftr 9992 iccshftl 9994 iccdil 9996 icccntr 9998 fzaddel 10056 elfzomelpfzo 10228 nnesq 10636 hashnncl 10770 zfz1isolemiso 10814 mod2eq1n2dvds 11878 m1exp1 11900 dfgcd3 12005 dvdssq 12026 pcdvdsb 12313 pceq0 12315 issubg3 13005 lmss 13639 lmres 13641 |
Copyright terms: Public domain | W3C validator |