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 608 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) |
3 | 2falsed.2 | . . 3 ⊢ (𝜑 → ¬ 𝜒) | |
4 | 3 | pm2.21d 608 | . 2 ⊢ (𝜑 → (𝜒 → 𝜓)) |
5 | 2, 4 | impbid 128 | 1 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → 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 ax-in2 604 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: pm5.21ni 692 bianfd 932 abvor0dc 3386 nn0eln0 4533 nntri3 6393 fin0 6779 omp1eomlem 6979 ctssdccl 6996 ismkvnex 7029 xrlttri3 9590 nltpnft 9604 ngtmnft 9607 xrrebnd 9609 xltadd1 9666 xposdif 9672 xleaddadd 9677 hashnncl 10549 zfz1isolemiso 10589 mod2eq1n2dvds 11583 m1exp1 11605 |
Copyright terms: Public domain | W3C validator |