![]() |
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 670 | 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 614 ax-in2 615 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: nnexmid 850 nndc 851 fal 1360 ax-9 1531 nonconne 2359 nemtbir 2436 ru 2961 noel 3426 iun0 3940 0iun 3941 br0 4048 vprc 4132 iin0r 4166 nlim0 4391 snnex 4445 onsucelsucexmid 4526 0nelxp 4651 dm0 4837 iprc 4891 co02 5138 0fv 5546 frec0g 6392 nnsucuniel 6490 1nen2 6855 fidcenumlemrk 6947 djulclb 7048 ismkvnex 7147 pw1ne3 7223 sucpw1nel3 7226 3nsssucpw1 7229 0nnq 7351 0npr 7470 nqprdisj 7531 0ncn 7818 axpre-ltirr 7869 pnfnre 7986 mnfnre 7987 inelr 8528 xrltnr 9763 fzo0 10151 fzouzdisj 10163 inftonninf 10424 hashinfom 10739 3prm 12108 sqrt2irr 12142 ennnfonelem1 12388 bj-nndcALT 14159 bj-vprc 14297 pwle2 14397 exmidsbthrlem 14419 |
Copyright terms: Public domain | W3C validator |