New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > mtbiri | GIF version |
Description: An inference from a biconditional, similar to modus tollens. (Contributed by NM, 24-Aug-1995.) |
Ref | Expression |
---|---|
mtbiri.min | ⊢ ¬ χ |
mtbiri.maj | ⊢ (φ → (ψ ↔ χ)) |
Ref | Expression |
---|---|
mtbiri | ⊢ (φ → ¬ ψ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mtbiri.min | . 2 ⊢ ¬ χ | |
2 | mtbiri.maj | . . 3 ⊢ (φ → (ψ ↔ χ)) | |
3 | 2 | biimpd 198 | . 2 ⊢ (φ → (ψ → χ)) |
4 | 1, 3 | mtoi 169 | 1 ⊢ (φ → ¬ ψ) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 176 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 177 |
This theorem is referenced by: psstr 3373 n0i 3555 pw10 4161 0nelsuc 4400 ltfinirr 4457 peano4 4557 addccan2 4559 phi011lem1 4598 ndmfvrcl 5350 xpnedisj 5513 oprssdm 5612 ndmovrcl 5616 ncssfin 6151 ncspw1eu 6159 nntccl 6170 ceclb 6183 ce0ncpw1 6185 cecl 6186 nclecid 6197 le0nc 6200 addlecncs 6209 nnc3n3p1 6278 |
Copyright terms: Public domain | W3C validator |