![]() |
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 9795 nltpnft 9812 ngtmnft 9815 xrrebnd 9817 xltadd1 9874 xposdif 9880 xleaddadd 9885 hashnncl 10770 zfz1isolemiso 10814 mod2eq1n2dvds 11878 m1exp1 11900 pceq0 12315 |
Copyright terms: Public domain | W3C validator |