![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 2falsed | GIF version |
Description: Two falsehoods are equivalent (deduction form). (Contributed by NM, 11-Oct-2013.) |
Ref | Expression |
---|---|
2falsed.1 | ⊢ (𝜑 → ¬ 𝜓) |
2falsed.2 | ⊢ (𝜑 → ¬ 𝜒) |
Ref | Expression |
---|---|
2falsed | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2falsed.1 | . . 3 ⊢ (𝜑 → ¬ 𝜓) | |
2 | 1 | pm2.21d 619 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) |
3 | 2falsed.2 | . . 3 ⊢ (𝜑 → ¬ 𝜒) | |
4 | 3 | pm2.21d 619 | . 2 ⊢ (𝜑 → (𝜒 → 𝜓)) |
5 | 2, 4 | impbid 129 | 1 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → 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 ax-in2 615 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: pm5.21ni 703 bianfd 948 abvor0dc 3446 nn0eln0 4619 nntri3 6497 fin0 6884 omp1eomlem 7092 ctssdccl 7109 ismkvnex 7152 xrlttri3 9796 nltpnft 9813 ngtmnft 9816 xrrebnd 9818 xltadd1 9875 xposdif 9881 xleaddadd 9886 hashnncl 10774 zfz1isolemiso 10818 mod2eq1n2dvds 11883 m1exp1 11905 pceq0 12320 |
Copyright terms: Public domain | W3C validator |