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 131 | . 2 ⊢ (𝜓 ↔ 𝜑) |
4 | 1, 3 | mtbi 644 | 1 ⊢ ¬ 𝜑 |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 ↔ wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 588 ax-in2 589 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: nnexmid 820 nndc 821 fal 1323 ax-9 1496 nonconne 2297 nemtbir 2374 ru 2881 noel 3337 iun0 3839 0iun 3840 br0 3946 vprc 4030 iin0r 4063 nlim0 4286 snnex 4339 onsucelsucexmid 4415 0nelxp 4537 dm0 4723 iprc 4777 co02 5022 0fv 5424 frec0g 6262 nnsucuniel 6359 1nen2 6723 fidcenumlemrk 6810 djulclb 6908 ismkvnex 6997 0nnq 7140 0npr 7259 nqprdisj 7320 0ncn 7607 axpre-ltirr 7658 pnfnre 7775 mnfnre 7776 inelr 8314 xrltnr 9534 fzo0 9913 fzouzdisj 9925 inftonninf 10182 hashinfom 10492 3prm 11736 sqrt2irr 11767 ennnfonelem1 11847 bj-nndcALT 12890 bj-vprc 13021 pwle2 13120 exmidsbthrlem 13144 |
Copyright terms: Public domain | W3C validator |