![]() |
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 633 | 1 ⊢ ¬ 𝜑 |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 ↔ wb 104 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 582 ax-in2 583 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: fal 1303 ax-9 1476 nonconne 2274 nemtbir 2351 ru 2853 noel 3306 iun0 3808 0iun 3809 vprc 3992 iin0r 4025 nlim0 4245 snnex 4298 onsucelsucexmid 4374 0nelxp 4495 dm0 4681 iprc 4733 co02 4978 0fv 5374 frec0g 6200 nnsucuniel 6296 1nen2 6657 fidcenumlemrk 6743 djulclb 6827 0nnq 7020 0npr 7139 nqprdisj 7200 0ncn 7466 axpre-ltirr 7514 pnfnre 7626 mnfnre 7627 inelr 8158 xrltnr 9349 fzo0 9728 fzouzdisj 9740 inftonninf 9996 hashinfom 10317 3prm 11552 sqrt2irr 11583 nnexmid 12372 nndc 12373 bj-vprc 12499 exmidsbthrlem 12621 |
Copyright terms: Public domain | W3C validator |