Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 2thd | GIF version |
Description: Two truths are equivalent (deduction rule). (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 171 | . 2 ⊢ (𝜓 → (𝜒 → (𝜓 ↔ 𝜒))) | |
4 | 1, 2, 3 | sylc 61 | 1 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 103 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: abvor0dc 3269 euotd 4009 nn0eln0 4359 elabrex 5418 riota5f 5512 nntri3 6098 fin0 6369 nn1m1nn 8057 xrlttri3 8872 nltpnft 8884 ngtmnft 8885 xrrebnd 8886 iccshftr 9016 iccshftl 9018 iccdil 9020 icccntr 9022 fzaddel 9077 elfzomelpfzo 9240 nnesq 9592 mod2eq1n2dvds 10279 m1exp1 10301 dfgcd3 10399 dvdssq 10420 |
Copyright terms: Public domain | W3C validator |