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 609 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) |
3 | 2falsed.2 | . . 3 ⊢ (𝜑 → ¬ 𝜒) | |
4 | 3 | pm2.21d 609 | . 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 605 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: pm5.21ni 693 bianfd 937 abvor0dc 3427 nn0eln0 4591 nntri3 6456 fin0 6842 omp1eomlem 7050 ctssdccl 7067 ismkvnex 7110 xrlttri3 9724 nltpnft 9741 ngtmnft 9744 xrrebnd 9746 xltadd1 9803 xposdif 9809 xleaddadd 9814 hashnncl 10698 zfz1isolemiso 10738 mod2eq1n2dvds 11801 m1exp1 11823 pceq0 12232 |
Copyright terms: Public domain | W3C validator |