![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mtbir | GIF version |
Description: An inference from a biconditional, related to modus tollens. (Contributed by NM, 15-Nov-1994.) (Proof shortened by Wolf Lammen, 14-Oct-2012.) |
Ref | Expression |
---|---|
mtbir.1 | ⊢ ¬ 𝜓 |
mtbir.2 | ⊢ (𝜑 ↔ 𝜓) |
Ref | Expression |
---|---|
mtbir | ⊢ ¬ 𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mtbir.1 | . 2 ⊢ ¬ 𝜓 | |
2 | mtbir.2 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
3 | 2 | bicomi 132 | . 2 ⊢ (𝜓 ↔ 𝜑) |
4 | 1, 3 | mtbi 671 | 1 ⊢ ¬ 𝜑 |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 ↔ wb 105 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: nnexmid 851 nndc 852 fal 1371 ax-9 1542 nonconne 2372 nemtbir 2449 ru 2976 noel 3441 iun0 3961 0iun 3962 br0 4069 vprc 4153 iin0r 4190 nlim0 4415 snnex 4469 onsucelsucexmid 4550 0nelxp 4675 dm0 4862 iprc 4916 co02 5163 0fv 5573 frec0g 6426 nnsucuniel 6524 1nen2 6893 fidcenumlemrk 6987 djulclb 7088 ismkvnex 7188 pw1ne3 7264 sucpw1nel3 7267 3nsssucpw1 7270 0nnq 7398 0npr 7517 nqprdisj 7578 0ncn 7865 axpre-ltirr 7916 pnfnre 8034 mnfnre 8035 inelr 8576 xrltnr 9815 fzo0 10204 fzouzdisj 10216 inftonninf 10479 hashinfom 10799 3prm 12171 sqrt2irr 12205 ennnfonelem1 12469 bj-nndcALT 14996 bj-vprc 15134 pwle2 15235 exmidsbthrlem 15258 |
Copyright terms: Public domain | W3C validator |