![]() |
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 130 | . 2 ⊢ (𝜓 ↔ 𝜑) |
4 | 1, 3 | mtbi 628 | 1 ⊢ ¬ 𝜑 |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 ↔ wb 103 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-in1 577 ax-in2 578 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: fal 1292 ax-9 1465 nonconne 2261 nemtbir 2338 ru 2825 noel 3273 iun0 3760 0iun 3761 vprc 3936 iin0r 3969 nlim0 4185 snnex 4235 onsucelsucexmid 4309 0nelxp 4428 dm0 4608 iprc 4659 co02 4898 0fv 5284 frec0g 6094 nnsucuniel 6188 1nen2 6507 djulclb 6654 0nnq 6826 0npr 6945 nqprdisj 7006 0ncn 7272 axpre-ltirr 7320 pnfnre 7432 mnfnre 7433 inelr 7961 xrltnr 9145 fzo0 9468 fzouzdisj 9480 inftonninf 9736 hashinfom 10021 3prm 10890 sqrt2irr 10921 nnexmid 11003 nndc 11004 bj-vprc 11130 exmidsbthrlem 11254 |
Copyright terms: Public domain | W3C validator |